Commit 29bf46f4 authored by POTTIER Francois's avatar POTTIER Francois

Added a random closed term generator.

parent 6219e27d
open Printf
open AlphaLib
open Term
open TermGenerator
module T = Toolbox.Make(Term)
open T
......@@ -148,3 +149,9 @@ let print_wf t =
let () =
evaluate print_wf;
print_wf (TApp (id, id))
let () =
for _i = 0 to 9 do
printf "generate() = %a\n%!"
hprint (import_term KitImport.empty (generate 10))
done
open Term
let split n =
assert (n >= 0);
let n1 = Random.int (n + 1) in
let n2 = n - n1 in
assert (0 <= n1 && n1 <= n);
assert (0 <= n2 && n2 <= n);
n1, n2
let random_variable () =
let i = Random.int 26 in
let c = Char.chr (Char.code 'a' + i) in
String.make 1 c
module StringSet =
Set.Make(String)
let random_set_element xs = (* inefficient *)
let n = StringSet.cardinal xs in
assert (n > 0);
let i = Random.int n in
List.nth (StringSet.elements xs) i
let rec generate env n =
assert (n >= 0);
assert (not (StringSet.is_empty env));
if n = 0 then
TVar (random_set_element env)
else
match Random.int 2 with
| 0 ->
let n1, n2 = split (n - 1) in
TApp (generate env n1, generate env n2)
| 1 ->
generate_lambda env n
| _ ->
assert false
and generate_lambda env n =
let n = n - 1 in
let x = random_variable () in
let env = StringSet.add x env in
TLambda (x, generate env n)
let generate n =
assert (n > 0);
(* Begin with [TLambda], so we have a nonempty [env]. *)
generate_lambda StringSet.empty n
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