Commit abf1da90 authored by SCHERER Gabriel's avatar SCHERER Gabriel
Browse files

Merge branch 'qcheck' into 'master'

Use QCheck for the random test suite

See merge request !25
parents 268b622a 64f309fc
Pipeline #249635 failed with stage
in 12 minutes and 8 seconds
open Client
let test ~log (env : F.nominal_datatype_env) (t : F.nominal_term) =
let test_with_log ~log (env : F.nominal_datatype_env) (t : F.nominal_term) =
Log.log_action log (fun () ->
Printf.printf "Formatting the System F term...\n%!";
let doc = PPrint.(FPrinter.print_term t ^^ hardline) in
......@@ -21,3 +21,14 @@ let test ~log (env : F.nominal_datatype_env) (t : F.nominal_term) =
in
()
let test (env : F.nominal_datatype_env) (t : F.nominal_term) =
let env : F.debruijn_datatype_env =
F.translate_env env in
let t : F.debruijn_term =
F.Term.translate t
in
let _ty : F.debruijn_type =
FTypeChecker.typeof env t
in
()
......@@ -33,7 +33,7 @@ let translate e t =
(* Running all passes over a single ML term. *)
let test ~log (env : ML.datatype_env) (t : ML.term) : bool =
let test_with_log ~log (env : ML.datatype_env) (t : ML.term) : bool =
(* We print the term, parse it and compare with the given term *)
let s = MLPrinter.to_string t in
let lexbuf = Lexing.from_string s in
......@@ -52,6 +52,29 @@ let test ~log (env : ML.datatype_env) (t : ML.term) : bool =
our terms can be randomly generated. *)
false
| Some (t : F.nominal_term) ->
CheckF.test ~log outcome_env t;
CheckF.test_with_log ~log outcome_env t;
(* Everything seems to be OK. *)
true
let test ~(success:int ref) ~(total:int ref) (env : ML.datatype_env) (t : ML.term) : bool =
incr total;
(* We print the term, parse it and compare with the given term *)
let s = MLPrinter.to_string t in
let lexbuf = Lexing.from_string s in
let t' = MLParser.self_contained_term MLLexer.read lexbuf in
assert (t = t');
let outcome_env =
ML2F.translate_env env in
let outcome =
translate env t
in
match outcome with
| None ->
(* This term is ill-typed. This is considered a normal outcome, since
our terms can be randomly generated. *)
true
| Some (t : F.nominal_term) ->
CheckF.test outcome_env t;
(* Everything seems to be OK. *)
incr success;
true
......@@ -175,14 +175,17 @@ let match_none = F.(
)
)
let test =
Test.(Log.with_log CheckF.test_with_log)
let () =
Test.(Log.with_log (CheckF.test Datatype.Env.empty) let_prod);
Test.(Log.with_log (CheckF.test Datatype.Env.empty) inj);
Test.(Log.with_log (CheckF.test Datatype.Env.empty) match_with_prod);
Test.(Log.with_log (CheckF.test Datatype.Env.empty) match_with_sum);
Test.(Log.with_log (CheckF.test Datatype.Env.empty) match_inj);
Test.(Log.with_log (CheckF.test option_env) unit);
Test.(Log.with_log (CheckF.test option_env) none);
Test.(Log.with_log (CheckF.test option_env) some);
Test.(Log.with_log (CheckF.test option_env) match_none);
test Datatype.Env.empty let_prod;
test Datatype.Env.empty inj;
test Datatype.Env.empty match_with_prod;
test Datatype.Env.empty match_with_sum;
test Datatype.Env.empty match_inj;
test option_env unit;
test option_env none;
test option_env some;
test option_env match_none;
print_endline "TestF: all tests passed."
......@@ -189,23 +189,24 @@ let node =
])
)
let test =
Test.(Log.with_log CheckML.test_with_log)
let () =
assert Test.(Log.with_log CheckML.test Datatype.Env.empty idid);
assert Test.(Log.with_log CheckML.test Datatype.Env.empty genid);
assert Test.(Log.with_log CheckML.test Datatype.Env.empty genidid);
assert Test.(Log.with_log CheckML.test Datatype.Env.empty genkidid);
assert Test.(Log.with_log CheckML.test Datatype.Env.empty genkidid2);
assert Test.(Log.with_log CheckML.test option_env none);
assert Test.(Log.with_log CheckML.test option_env some);
assert Test.(Log.with_log CheckML.test list_env nil);
assert Test.(Log.with_log CheckML.test list_env list);
assert Test.(Log.with_log CheckML.test list_env list_annotated);
assert Test.(Log.with_log CheckML.test tree_env leaf);
assert Test.(Log.with_log CheckML.test tree_env node);
assert Test.(Log.with_log CheckML.test Datatype.Env.empty abs_match_with);
assert Test.(Log.with_log CheckML.test option_env match_none);
assert Test.(Log.with_log CheckML.test option_env match_some);
assert Test.(Log.with_log CheckML.test option_env match_some_annotated);
assert (test Datatype.Env.empty idid);
assert (test Datatype.Env.empty genid);
assert (test Datatype.Env.empty genidid);
assert (test Datatype.Env.empty genkidid);
assert (test Datatype.Env.empty genkidid2);
assert (test option_env none);
assert (test option_env some);
assert (test list_env nil);
assert (test list_env list);
assert (test tree_env leaf);
assert (test tree_env node);
assert (test Datatype.Env.empty abs_match_with);
assert (test option_env match_none);
assert (test option_env match_some);
(* we include some printing below because Dune
appears to only show tests that show some output. *)
print_endline "TestML: all tests passed."
......@@ -245,7 +246,7 @@ let test_from_string typedecl s expected on_same on_different on_error =
| Ok (datatype_env, t) ->
if t = expected then
begin
assert Test.(Log.with_log CheckML.test datatype_env t);
assert (test datatype_env t);
on_same ();
end
else
......
......@@ -10,41 +10,11 @@ let int2var k =
(* [split n] produces two numbers [n1] and [n2] comprised between [0] and [n]
(inclusive) whose sum is [n]. *)
let split n =
let n1 = Random.int (n + 1) in
let split n st =
let n1 = Random.State.int st (n + 1) in
let n2 = n - n1 in
n1, n2
(* The parameter [k] is the number of free variables; the parameter [n] is the
size (i.e., the number of internal nodes). *)
let rec random_ml_term k n =
if n = 0 then begin
assert (k > 0);
ML.Var (int2var (Random.int k))
end
else
let c = Random.int 5 (* Abs, App, Pair, Let, LetProd *) in
if k = 0 || c = 0 then
(* The next available variable is [k]. *)
let x, k = int2var k, k + 1 in
ML.Abs (x, random_ml_term k (n - 1))
else if c = 1 then
let n1, n2 = split (n - 1) in
ML.App (random_ml_term k n1, random_ml_term k n2)
else if c = 2 then
let n1, n2 = split (n - 1) in
ML.Tuple [random_ml_term k n1; random_ml_term k n2]
else if c = 3 then
let n1, n2 = split (n - 1) in
ML.Let (int2var k, random_ml_term k n1, random_ml_term (k + 1) n2)
else if c = 4 then
let n1, n2 = split (n - 1) in
let x1, x2, k' = int2var k, int2var (k + 1), k + 2 in
ML.LetProd ([x1; x2], random_ml_term k n1, random_ml_term k' n2)
else
assert false
let rec size accu = function
| ML.Var _
| ML.Variant (_, None)
......@@ -81,6 +51,196 @@ and size_pattern accu = function
let size =
size 0
(* -------------------------------------------------------------------------- *)
(* A random term generator using QCheck. *)
let var x = ML.Var (int2var x)
(* In the following functions, the parameter [k] is the number of free
variables; the parameter [n] is the size (i.e., the number of
internal nodes). *)
let abs k n self = QCheck.Gen.(
let+ (x,t) = pair (int2var <$> pure k) (self (k + 1, n - 1))
in ML.Abs (x, t)
)
let app k n self = QCheck.Gen.(
let* n1, n2 = split (n - 1) in
let+ (t1, t2) = pair (self (k, n1)) (self (k, n2))
in ML.App (t1, t2)
)
let tuple k n self = QCheck.Gen.(
let* n1, n2 = split (n - 1) in
let+ (t1, t2) = pair (self (k, n1)) (self (k, n2))
in ML.Tuple [t1; t2]
)
let let_ k n self = QCheck.Gen.(
let* n1, n2 = split (n - 1) in
let+ (x,t1,t2) =
triple (int2var <$> pure k) (self (k, n1)) (self (k+1, n2))
in ML.Let (x, t1, t2)
)
let let_prod k n self = QCheck.Gen.(
let* n1, n2 = split (n - 1) in
let+ (x1,x2,t1,t2) =
quad
(int2var <$> pure k)
(int2var <$> pure (k + 1))
(self (k, n1))
(self (k+2, n2))
in ML.LetProd ([x1; x2], t1, t2)
)
let term_gen = QCheck.Gen.(
fix
(fun self (k, n) ->
if n = 0 then begin
assert (k > 0);
var <$> (int_bound (k-1))
end
else
if k = 0 then
abs k n self
else
frequency
[
1, abs k n self ;
1, app k n self ;
1, tuple k n self ;
1, let_ k n self ;
1, let_prod k n self ;
]
)
)
(* -------------------------------------------------------------------------- *)
(* Shrinker. *)
module Shrinker = struct
module Shrink = QCheck.Shrink
module Iter = QCheck.Iter
let rec fv x = function
| ML.Var y ->
x = y
| ML.Abs (y, t) ->
if x = y then false
else fv x t
| ML.App (t1, t2) ->
fv x t1 || fv x t2
| ML.Let (y, t, u) ->
fv x t || (x <> y && fv x u)
| ML.Tuple ts ->
List.exists (fv x) ts
| ML.LetProd (xs, t, u) ->
fv x t || (List.for_all ((<>) x) xs && fv x u)
| ML.Annot (t, _)
| ML.Variant (_, Some t) ->
fv x t
| ML.Variant (_, None) ->
false
| ML.Match (t, brs) ->
fv x t || List.exists (fv_br x) brs
and fv_br x (pat, t) =
if bv_pat x pat then
false
else
fv x t
and bv_pat x = function
| PVar y ->
x = y
| PWildcard ->
false
| PAnnot (pat, _)
| PVariant (_, Some pat) ->
bv_pat x pat
| PVariant (_, None) ->
false
| PTuple ps ->
List.exists (bv_pat x) ps
let (let+) a f = Iter.map f a
let rec shrink_term gamma t = Iter.(
(match t, List.rev gamma with
| ML.Var _, _ ->
empty
| _, x0 :: _ ->
return (ML.Var x0)
| _, [] ->
empty
) <+> (
match t with
| ML.Var _ ->
empty
| ML.Abs (x, t) ->
let t' = shrink_term (x::gamma) t in
(if fv x t then empty else return t)
<+> (let+ t' = t' in ML.Abs (x, t'))
| ML.App (t1, t2) ->
let t1' = shrink_term gamma t1 in
let t2' = shrink_term gamma t2 in
return t1
<+> t2'
<+> (let+ t1' = t1' and+ t2' = t2' in ML.App (t1',t2'))
| ML.Let (x, t, u) ->
let t' = shrink_term gamma t in
let u' = shrink_term (x::gamma) u in
return t
<+> (if fv x u then empty else return u)
<+> (let+ t' = t' and+ u' = u' in ML.Let (x, t', u'))
| ML.LetProd (xs, t, u) ->
let t' = shrink_term gamma t in
let u' = shrink_term (xs@gamma) u in
return t
(* A more clever approach would be to inspect [t] to see if it is a
tuple and decrease the size of the tuple and the number of variables
in the let-binding, when the variable isn't free in the body.
For instance
let (x, y, z) = (t1, t2, t3) in x z
can be shrunk into
let (x, z) = (t1, t3) in x z
*)
<+> (let xs' = List.filter (fun x -> fv x u) xs in
if List.length xs == List.length xs' then
empty
else
match xs' with
| [] ->
return u
| _ ->
return (ML.LetProd (xs', t, u))
)
<+> (let+ t' = t' and+ u' = u' in ML.LetProd (xs, t', u'))
| ML.Tuple ts ->
of_list ts
<+> let+ ts' = Shrink.list ~shrink:(shrink_term gamma) ts
in ML.Tuple ts'
| _ ->
assert false
)
)
end
(* -------------------------------------------------------------------------- *)
(* Random testing. *)
......@@ -113,18 +273,33 @@ let pairs =
let () =
Printf.printf "Preparing to type-check a bunch of randomly-generated terms...\n%!";
Random.init 0;
let c = ref 0 in
let d = ref 0 in
List.iter (fun (m, n) ->
for i = 1 to m do
if Test.Config.verbose then
Printf.printf "Test number %d...\n%!" i;
let t = random_ml_term 0 n in
assert (size t = n);
let success = Test.(Log.with_log CheckML.test Datatype.Env.empty t) in
if success then incr c;
incr d
done
) pairs;
Printf.printf "In total, %d out of %d terms were considered well-typed.\n%!" !c !d;
let count_success = ref 0 in
let count_total = ref 0 in
let tests =
List.map (fun (m, n) ->
let arb =
QCheck.make
~print:MLPrinter.to_string
~shrink:(Shrinker.shrink_term [])
(term_gen (0, n))
in
let prop t =
Test.CheckML.test
~success:count_success
~total:count_total
Datatype.Env.empty
t
in
QCheck.Test.make
~name:(Printf.sprintf "Type checking (size %d)" n)
~count:m
arb
prop
) pairs in
QCheck_runner.set_seed 0;
let _ = QCheck_runner.run_tests ~colors:true ~verbose:true tests in
Printf.printf
"In total, %d out of %d terms (%.1f%%) were considered well-typed.\n%!"
!count_success !count_total
(float !count_success /. float !count_total *. 100.);
Printf.printf "No problem detected.\n%!"
......@@ -19,6 +19,6 @@
(test
(name TestMLRandom)
(libraries client test)
(libraries client test qcheck)
(modules TestMLRandom)
)
......@@ -24,4 +24,5 @@ depends: [
# package to make the distinction clearer.
"menhir" {with-test}
"pprint" {with-test}
"qcheck" {with-test}
]
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment