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

TestMLRandom: generate trivial annotations

This trivial annotation is useful to test the translation of
annotations from ML to System F: the annotation (t : some a. a) should
be elaborated into an annotation (t : ty) where (ty) is the inferred
type for (t).
parent 5e6ab385
Pipeline #259253 passed with stage
in 8 minutes and 7 seconds
......@@ -98,6 +98,11 @@ let let_prod k n self = QCheck.Gen.(
in ML.LetProd ([x1; x2], t1, t2)
)
let annot k n self = QCheck.Gen.(
let+ t = self (k, n-1) in
ML.Annot (t, (["'a"], ML.TyVar "'a"))
)
let term_gen = QCheck.Gen.(
fix
(fun self (k, n) ->
......@@ -116,6 +121,7 @@ let term_gen = QCheck.Gen.(
1, tuple k n self ;
1, let_ k n self ;
1, let_prod k n self ;
1, annot k n self ;
]
)
)
......
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