Commit eedfd95c authored by Gabriel Scherer's avatar Gabriel Scherer
Browse files

shrinking: a 'subterms' abstraction over Hole

parent 51298a91
Pipeline #252002 passed with stage
in 19 minutes and 16 seconds
......@@ -198,6 +198,14 @@ module Shrinker = struct
(let+ a' = ita in (a', b))
(let+ b' = itb in (a, b'))
in
let subterms ts =
(* ...[t1, t2] is not always a desirable shrinking choice for a term
containing [t1, t2] as subterms, because it breaks the property that
the types of t1 and t2 appear in the resulting type, which is sometimes
important to reproduce typing bugs.
So we start with just (t1) and (t2) as shrinking choices,
even though they typically do not preserve typability. *)
of_list ts <+> return (ML.Hole ts) in
(match t with
| ML.Hole [] ->
empty
......@@ -216,14 +224,14 @@ module Shrinker = struct
)
| ML.Abs (x, t) ->
(return (remove_variable t x))
subterms [remove_variable t x]
<+> (
let+ t' = shrink_term t in
ML.Abs (x, t')
)
| ML.App (t1, t2) ->
return (ML.Hole [t1; t2])
subterms [t1; t2]
<+> (
let++ t1' = t1, shrink_term t1
and++ t2' = t2, shrink_term t2
......@@ -231,7 +239,7 @@ module Shrinker = struct
)
| ML.Let (x, t, u) ->
return (ML.Hole [t; remove_variable u x])
subterms [t; remove_variable u x]
<+> (
let++ t' = t, shrink_term t
and++ u' = u, shrink_term u
......@@ -239,7 +247,7 @@ module Shrinker = struct
)
| ML.LetProd (xs, t, u) ->
return (ML.Hole [t; remove_variables u xs])
subterms [t; remove_variables u xs]
<+> (match t with
| ML.Hole _ ->
let+ xs' = Shrink.list_spine xs in
......@@ -258,17 +266,17 @@ module Shrinker = struct
)
| ML.Tuple ts ->
return (ML.Hole ts)
subterms ts
<+> (
let+ ts' = Shrink.list ~shrink:shrink_term ts
in ML.Tuple ts'
)
| ML.Annot (t, _ty) ->
return t
subterms [t]
| ML.Variant (lab, t) ->
return (ML.Hole (Option.to_list t))
subterms (Option.to_list t)
<+> (
match t with
| None -> empty
......
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