418 lines
21 KiB
OCaml
418 lines
21 KiB
OCaml
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)) );
|
|
]
|
|
|
|
let anf text = Anf.program (specialize text)
|
|
|
|
let anf_cases =
|
|
[
|
|
( "the example query normalizes to a chain of collection temporaries",
|
|
fun () ->
|
|
Ident.reset ();
|
|
Anf.reset ();
|
|
let program = anf (read_fixture "expensive_order.delta") in
|
|
Anf.validate [ program.Anf.ap_input ] program.Anf.ap_query_body;
|
|
(match program.Anf.ap_query_body with
|
|
| { Anf.a = Anf.ALet (filter_temp, filter, { Anf.a = Anf.ALet (map_temp, mapper, tail); _ }); _ }
|
|
->
|
|
check "the first temporary is a filter"
|
|
(match filter.Anf.a with Anf.AFilter _ -> true | _ -> false);
|
|
check "the second temporary is a map"
|
|
(match mapper.Anf.a with Anf.AMap _ -> true | _ -> false);
|
|
check "the query returns the map temporary"
|
|
(match tail.Anf.a with
|
|
| Anf.AAtom (Anf.AVar ident) -> Ident.equal ident map_temp
|
|
| _ -> false);
|
|
ignore filter_temp
|
|
| _ -> fail "shape" "expected two collection temporaries") );
|
|
( "every operand of a sum is an atom",
|
|
fun () ->
|
|
Anf.reset ();
|
|
let program = anf (read_fixture "revenue.delta") in
|
|
Anf.validate [ program.Anf.ap_input ] program.Anf.ap_query_body;
|
|
(match program.Anf.ap_query_body with
|
|
| { Anf.a = Anf.ALet (_, mapped, { Anf.a = Anf.ALet (_, summed, _); _ }); _ } ->
|
|
check "map temporary" (match mapped.Anf.a with Anf.AMap _ -> true | _ -> false);
|
|
check "sum uses an atom operand" (match summed.Anf.a with Anf.ASum _ -> true | _ -> false)
|
|
| _ -> fail "shape" "expected a map temporary then a sum") );
|
|
( "arithmetic arguments are bound to temporaries",
|
|
fun () ->
|
|
Anf.reset ();
|
|
let program = anf "input rows : collection int\nquery q = rows |> map (fun r -> r * 2 + r) |> sum\n" in
|
|
Anf.validate [ program.Anf.ap_input ] program.Anf.ap_query_body;
|
|
let dump = Anf.program_to_string program in
|
|
check "the dump binds a multiplication before the addition"
|
|
(Util.starts_with "input rows : collection int" dump);
|
|
check "the dump mentions the map operation" (String.length dump > 0) );
|
|
( "anf dumps are deterministic",
|
|
fun () ->
|
|
Ident.reset ();
|
|
Types.reset ();
|
|
Anf.reset ();
|
|
let first = Anf.program_to_string (anf (read_fixture "count_large.delta")) in
|
|
Ident.reset ();
|
|
Types.reset ();
|
|
Anf.reset ();
|
|
let second = Anf.program_to_string (anf (read_fixture "count_large.delta")) in
|
|
check_equal_string "identical" first second );
|
|
( "anf validation rejects duplicated binders",
|
|
fun () ->
|
|
let ident = Ident.fresh "x" Location.none in
|
|
let body =
|
|
Anf.{
|
|
a = ALet (ident, { a = AAtom (AInt 1); aty = Types.TInt; aspan = Location.none },
|
|
{ a = ALet (ident, { a = AAtom (AInt 2); aty = Types.TInt; aspan = Location.none },
|
|
{ a = AAtom (AInt 3); aty = Types.TInt; aspan = Location.none });
|
|
aty = Types.TInt; aspan = Location.none });
|
|
aty = Types.TInt;
|
|
aspan = Location.none;
|
|
}
|
|
in
|
|
(try
|
|
Anf.validate [] body;
|
|
fail "validate" "expected the invariant check to fail"
|
|
with Diagnostic.Error diagnostic ->
|
|
check "mentions a duplicated binder"
|
|
(Util.starts_with "anf invariant violated" diagnostic.Diagnostic.message)) );
|
|
( "anf validation rejects unbound uses",
|
|
fun () ->
|
|
let unbound = Ident.fresh "missing" Location.none in
|
|
let body =
|
|
Anf.
|
|
{
|
|
a = AAtom (AVar unbound);
|
|
aty = Types.TInt;
|
|
aspan = Location.none;
|
|
}
|
|
in
|
|
(try
|
|
Anf.validate [] body;
|
|
fail "validate" "expected the invariant check to fail"
|
|
with Diagnostic.Error diagnostic ->
|
|
check "mentions an unbound variable"
|
|
(Util.starts_with "anf invariant violated" diagnostic.Diagnostic.message)) );
|
|
]
|