Commit ccce10b5 authored by POTTIER Francois's avatar POTTIER Francois

Added a generator of nominal terms.

parent 194f2140
......@@ -144,8 +144,14 @@ let () =
let () =
for _i = 0 to 9 do
let t = import_term KitImport.empty (generate 15) in
printf "generate() = %a\n%!" hprint t;
let t = import_term KitImport.empty (generate_raw 15) in
printf "generate_raw() = %a\n%!" hprint t;
assert (closed_term t);
assert (Atom.Set.is_empty (fa_term t));
done
let () =
for _i = 0 to 9 do
let t = generate_nominal (* atoms: *) 5 (* size: *) 15 in
printf "generate_nominal() = %a\n%!" nhprint t
done
......@@ -3,6 +3,9 @@ open Term
module StringSet =
OST.Make(String)
module AtomSet =
OST.Make(AlphaLib.Atom)
(* Randomly split an integer [n] into [n1 + n2]. *)
let split n =
......@@ -20,7 +23,10 @@ let random_name () =
let c = Char.chr (Char.code 'a' + i) in
String.make 1 c
let rec generate env n =
(* Randomly generate a raw term whose free names are in the set [env]
and whose size is exactly [n]. *)
let rec generate_raw env n =
assert (n >= 0);
assert (StringSet.cardinal env > 0);
if n = 0 then
......@@ -29,19 +35,65 @@ let rec generate env n =
match Random.int 2 with
| 0 ->
let n1, n2 = split (n - 1) in
TApp (generate env n1, generate env n2)
TApp (generate_raw env n1, generate_raw env n2)
| 1 ->
generate_lambda env n
generate_raw_lambda env n
| _ ->
assert false
and generate_lambda env n =
and generate_raw_lambda env n =
assert (n > 0);
let n = n - 1 in
let x = random_name () in
let env = StringSet.add x env in
TLambda (x, generate env n)
TLambda (x, generate_raw env n)
let generate n =
(* Randomly generate a closed raw term of size [n]. *)
let generate_raw n =
assert (n > 0);
(* Begin with [TLambda], so we have a nonempty [env]. *)
generate_lambda StringSet.empty n
generate_raw_lambda StringSet.empty n
(* Randomly generate a nominal term whose bound and free names are in the set [env]
and whose size is [n]. *)
let rec generate_nominal env n =
assert (n >= 0);
assert (AtomSet.cardinal env > 0);
if n = 0 then
TVar (AtomSet.pick env)
else
match Random.int 2 with
| 0 ->
let n1, n2 = split (n - 1) in
TApp (generate_nominal env n1, generate_nominal env n2)
| 1 ->
generate_nominal_lambda env n
| _ ->
assert false
and generate_nominal_lambda env n =
assert (n > 0);
let n = n - 1 in
let x = AtomSet.pick env in
TLambda (x, generate_nominal env n)
(* Generate a set of [k] fresh atoms. *)
let rec atoms accu k =
if k = 0 then
accu
else
let a = AlphaLib.Atom.freshh "a" in
atoms (AtomSet.add a accu) (k - 1)
let atoms =
atoms AtomSet.empty
(* Randomly generate a nominal term whose bound and free names are taken from a set
of [k] fresh atoms and whose size is [n]. Note that this term does not satisfy
the GUH. *)
let generate_nominal k n =
generate_nominal (atoms k) 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