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

Merge branch 'typed-holes' into 'master'

typed holes (with subterms) for shrinking

See merge request !27
parents abf1da90 eedfd95c
Pipeline #258700 passed with stage
in 8 minutes and 11 seconds
......@@ -52,6 +52,7 @@ type tevar = string
type ('a, 'b) term =
| Var of tevar
| Hole of ('a, 'b) typ * ('a, 'b) term list
| Abs of tevar * ('a, 'b) typ * ('a, 'b) term
| App of ('a, 'b) term * ('a, 'b) term
| Let of tevar * ('a, 'b) term * ('a, 'b) term
......@@ -169,6 +170,10 @@ module TypeInTerm : DeBruijn.TRAVERSE
match t with
| Var x ->
Var x
| Hole (ty, ts) ->
let ty' = TypeInType.traverse lookup extend env ty in
let ts' = List.map (trav env) ts in
Hole (ty', ts')
| Abs (x, ty, t) ->
let ty' = TypeInType.traverse lookup extend env ty
and t' = trav env t in
......
......@@ -56,6 +56,7 @@ type tevar =
type ('a, 'b) term =
| Var of tevar
| Hole of ('a, 'b) typ * ('a, 'b) term list
| Abs of tevar * ('a, 'b) typ * ('a, 'b) term
| App of ('a, 'b) term * ('a, 'b) term
| Let of tevar * ('a, 'b) term * ('a, 'b) term
......
......@@ -35,6 +35,8 @@ let rec translate_term env (t : F.nominal_term) : P.term =
match t with
| F.Var x ->
P.Var x
| F.Hole (ty, ts) ->
P.Hole (Some (translate_type env ty), List.map (self env) ts)
| F.Abs (x, ty, t) ->
let annot = P.PAnnot (P.PVar x, ([], translate_type env ty)) in
P.Abs (annot, self env t)
......
......@@ -202,6 +202,11 @@ let rec typeof datatype_env env (t : debruijn_term) : debruijn_type =
match t with
| Var x ->
lookup env x
| Hole (ty, ts) ->
let on_subterm t =
ignore (typeof env t) in
List.iter on_subterm ts;
ty
| Abs (x, ty1, t) ->
let ty2 = typeof (extend_with_tevar env x ty1) t in
TyArrow (ty1, ty2)
......
......@@ -421,6 +421,19 @@ let hastype (typedecl_env : ML.datatype_env) (t : ML.term) (w : variable) : F.no
and+ ty = witness w
in F.Match (ty, t, branches')
| ML.Hole ts ->
(* A hole ...[t1, t2, .., tn] has any type, and its subterms
[t1, .., tn] can themselves have any type; our return type
w is unconstrained and we type each ti at a new inference
variable. *)
let on_subterm t k =
let@ v = exist in
k (hastype t v) in
let@ ts' = mapM_later on_subterm ts in
let+ ts' = ts'
and+ ty = witness w
in F.Hole (ty, ts')
and hastype_variant typedecl_env c w
: (F.nominal_datatype co * variable, 'r) binder
= fun k ->
......
......@@ -18,6 +18,7 @@ type type_annotation = tyvar list * typ
type term =
| Var of tevar
| Hole of term list
| Abs of tevar * term
| App of term * term
| Let of tevar * term * term
......
......@@ -43,6 +43,8 @@ rule read =
| ')' { RPAR }
| '{' { LBRACE }
| '}' { RBRACE }
| '[' { LBRACKET }
| ']' { RBRACKET }
| '*' { STAR }
| ',' { COMMA }
| '_' { WILDCARD }
......@@ -50,5 +52,6 @@ rule read =
| '=' { EQ }
| ":" { COLON }
| '.' { PERIOD }
| "..." { DOTS }
| eof { EOF }
| _ as c { failwith (Printf.sprintf "Unexpected character during lexing: %c" c) }
\ No newline at end of file
| _ as c { failwith (Printf.sprintf "Unexpected character during lexing: %c" c) }
......@@ -20,6 +20,10 @@
%token RBRACE "}"
%token STAR "*"
%token DOTS "..."
%token LBRACKET "["
%token RBRACKET "]"
%token COMMA
%token WILDCARD
%token PIPE
......@@ -85,6 +89,9 @@ let term_atom :=
brs = branches ;
END ; { Match (t, brs) }
| "..."; "["; ts = item_sequence(term, COMMA); "]";
{ Hole ts }
| "(" ; t = term ; ":" ; tyannot = type_annotation ; ")" ;
{ Annot (t, tyannot) }
......@@ -179,14 +186,16 @@ let tyvar :=
| ~ = QIDENT ; <>
let tuple (X) :=
| "(" ; ")" ; { [] }
| "(" ; x = X ; COMMA ; xs = inside_tuple (X) ; ")" ;
{ x :: xs }
let inside_tuple (X) :=
| { [] }
| x = X ; { [x] }
| x = X ; COMMA ; xs = inside_tuple(X); { x :: xs }
| "(" ; ")" ; { [] }
(* note: the rule below enforces that one-element lists always
end with a trailing comma *)
| "(" ; x = X ; COMMA ; xs = item_sequence(X, COMMA) ; ")"; { x :: xs }
(* item sequence with optional trailing separator *)
let item_sequence(X, Sep) :=
| { [] }
| x = X ; { [x] }
| x = X ; () = Sep ; xs = item_sequence(X, Sep); { x :: xs }
let letin (X) :=
| LET ; x = X ; EQ ;
......
......@@ -25,6 +25,8 @@ let rec translate_term (t : ML.term) : P.term =
match t with
| ML.Var x ->
P.Var x
| ML.Hole ts ->
P.Hole (None, List.map self ts)
| ML.Abs (x, t) ->
P.Abs (P.PVar x, self t)
| ML.App (t1, t2) ->
......
......@@ -20,6 +20,7 @@ type tevar = string
type term =
| Var of tevar
| Hole of typ option * term list
| Abs of pattern * term
| App of term * term
| Let of pattern * term * term
......
......@@ -173,6 +173,10 @@ and print_term_atom t =
group @@ match t with
| Var x ->
print_tevar x
| Hole (ty, ts) ->
optional print_angle_type ty
^^ string "..."
^^ surround_separate_map 2 0 (lbracket ^^ rbracket) lbracket (comma ^^ break 1) rbracket print_term ts
| Tuple ts ->
print_tuple print_term ts
| Match (ty, t, brs) ->
......
......@@ -28,6 +28,7 @@ let rec size accu = function
| ML.LetProd (_, t1, t2)
-> size (size (accu + 1) t1) t2
| ML.Tuple ts
| ML.Hole ts
-> List.fold_left size (accu + 1) ts
| ML.Match (t, brs)
-> List.fold_left size_branch (size (accu + 1) t) brs
......@@ -127,116 +128,166 @@ module Shrinker = struct
module Shrink = QCheck.Shrink
module Iter = QCheck.Iter
let rec fv x = function
let rec bv_pat = function
| ML.PVar y -> [y]
| ML.PWildcard | ML.PVariant (_, None) -> []
| ML.PAnnot (pat, _)
| ML.PVariant (_, Some pat) ->
bv_pat pat
| ML.PTuple ps ->
List.concat_map bv_pat ps
(* t[u/x] *)
let rec subst t x u =
match t with
| ML.Var y ->
x = y
if x = y then u
else ML.Var y
| ML.Abs (y, t) ->
if x = y then false
else fv x t
ML.Abs (y, subst_under [y] t x u)
| ML.App (t1, t2) ->
fv x t1 || fv x t2
| ML.Let (y, t, u) ->
fv x t || (x <> y && fv x u)
ML.App (subst t1 x u, subst t2 x u)
| ML.Let (y, t1, t2) ->
ML.Let (y, subst t1 x u, subst_under [y] t2 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.Tuple (List.map (fun t -> subst t x u) ts)
| ML.Hole ts ->
ML.Hole (List.map (fun t -> subst t x u) ts)
| ML.LetProd (ys, t1, t2) ->
ML.LetProd (ys, subst t1 x u, subst_under ys t2 x u)
| ML.Annot (t, ty) ->
ML.Annot (subst t x u, ty)
| ML.Variant (ty, t) ->
ML.Variant (ty, Option.map (fun t -> subst t x u) t)
| 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)
| _, [] ->
ML.Match (subst t x u, List.map (fun br -> subst_branch br x u) brs)
(* (y.t)[u/x] *)
and subst_under ys t x u =
if List.mem x ys then t
else subst t x u
and subst_under_pat p t x u =
subst_under (bv_pat p) t x u
and subst_branch (p, t) x u =
(p, subst_under_pat p t x u)
let remove_variable t x =
subst t x (Hole [])
let remove_variables t xs =
List.fold_left remove_variable t xs
let rec shrink_term t = Iter.(
(* The Iter product is not suitable for shrinking:
(and+) (shrink a) (shrink b)
will try to shrink *both* a and b simultaneously,
but never try to shrink just one of them.
We shadow this unsuitable operator and use a "pointed product" (and++),
which tries to shrink a (with b constant) and then b (with a constant).
This corresponds to the behavior of Shrink.pair, but Shrink.pair works
on function types ('a -> 'a Iter.t), which is inconvenient
to write shrinkers directly -- no 'map' function. *)
let (and+) = () in ignore ((and+));
let (let++) (_a, it) f = Iter.map f it in
let (and++) (a, ita) (b, itb) =
(a, b),
Iter.append
(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
| _ ->
return (ML.Hole [])
) <+> (
match t with
| ML.Var _ ->
empty
| ML.Hole ts ->
(match ts with [t] -> return t | _ -> empty)
<+> (
let+ ts' = Shrink.list ~shrink:shrink_term ts
in ML.Hole ts'
)
| 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'))
subterms [remove_variable t x]
<+> (
let+ t' = shrink_term 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'))
subterms [t1; t2]
<+> (
let++ t1' = t1, shrink_term t1
and++ t2' = t2, shrink_term 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'))
subterms [t; remove_variable u x]
<+> (
let++ t' = t, shrink_term t
and++ u' = u, shrink_term 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'))
subterms [t; remove_variables u xs]
<+> (match t with
| ML.Hole _ ->
let+ xs' = Shrink.list_spine xs in
let u =
List.filter (fun x -> not (List.mem x xs')) xs
|> remove_variables u
in
if xs' = [] then u
else ML.LetProd (xs', t, u)
| _ -> empty
)
<+> (
let++ t' = t, shrink_term t
and++ u' = u, shrink_term 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'
subterms ts
<+> (
let+ ts' = Shrink.list ~shrink:shrink_term ts
in ML.Tuple ts'
)
| ML.Annot (t, _ty) ->
subterms [t]
| ML.Variant (lab, t) ->
subterms (Option.to_list t)
<+> (
match t with
| None -> empty
| Some t ->
let+ t' = shrink_term t
in ML.Variant (lab, Some t')
)
| ML.Match (_t, _branches) ->
failwith "unsupported"
| _ ->
assert false
)
)
end
......@@ -280,7 +331,7 @@ let () =
let arb =
QCheck.make
~print:MLPrinter.to_string
~shrink:(Shrinker.shrink_term [])
~shrink:Shrinker.shrink_term
(term_gen (0, n))
in
let prop t =
......@@ -297,7 +348,8 @@ let () =
prop
) pairs in
QCheck_runner.set_seed 0;
let _ = QCheck_runner.run_tests ~colors:true ~verbose:true tests in
let debug_shrink = None (* use (Some stdout) for a shrinking trace *) in
let _ = QCheck_runner.run_tests ~colors:true ~verbose:true ~debug_shrink tests in
Printf.printf
"In total, %d out of %d terms (%.1f%%) were considered well-typed.\n%!"
!count_success !count_total
......
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