The beginning of a more serious test suite.

demos/basic/Main.ml

@@ -2,9 +2,120 @@ open Printf
 open AlphaLib
 open Term
 open TermGenerator
-module T = Toolbox.Make(Term)
+
+module T =
+  Toolbox.Make(Term)
+
 open T
 
+(* [interval i j] constructs a list representation of the semi-open interval
+   [i..j). *)
+
+let rec interval i j : int list =
+  if i < j then
+    i :: interval (i + 1) j
+  else
+    []
+
+(* [init i j f] constructs a list of the values [f i] up to [f (j - 1)]. *)
+
+let init i j (f : int -> 'a) : 'a list =
+  List.map f (interval i j)
+
+(* A non-hygienic printer of arbitrary terms. This printer shows the internal
+   identity of atoms, using [Atom.show]. *)
+
+let nhprint oc t =
+  Print.term oc (show_term t)
+
+(* A hygienic printer of closed terms. This printer uses [export]. *)
+
+let hprint oc t =
+  Print.term oc (export_term KitExport.empty t)
+
+(* Test parameters. *)
+
+let number = 1000
+let size   = 1000
+let atoms  = 100
+
+(* A collection of closed raw terms. *)
+
+let closed_raw_terms : raw_term list =
+  printf "Generating random closed raw terms...\n%!";
+  init 0 number (fun _i ->
+    generate_raw size
+  )
+
+(* Import them, so as to obtain a collection of closed nominal terms. *)
+
+let closed_nominal_terms : nominal_term list =
+  printf "Importing these raw terms...\n%!";
+  List.map (import_term KitImport.empty) closed_raw_terms
+
+let on_closed_nominal_terms f =
+  List.iter f closed_nominal_terms
+
+(* The closed terms should be closed and well-formed. *)
+
+let () =
+  printf "Checking closedness and well-formedness...\n%!";
+  on_closed_nominal_terms (fun t ->
+    assert (closed_term t);
+    assert (Atom.Set.is_empty (fa_term t));
+    assert (wf_term t)
+  )
+
+(* A collection of random (non-closed, non-well-formed) nominal terms. *)
+
+let arbitrary_nominal_terms : nominal_term list =
+  printf "Generating random nominal terms...\n%!";
+  init 0 number (fun _i ->
+    generate_nominal atoms size
+  )
+
+let on_arbitrary_nominal_terms f =
+  List.iter f arbitrary_nominal_terms
+
+(* Copy them, so as to obtain well-formed (although non-closed) nominal terms. *)
+
+let wf_nominal_terms : nominal_term list =
+  printf "Copying these terms...\n%!";
+  List.map copy_term arbitrary_nominal_terms
+
+let on_wf_nominal_terms f =
+  List.iter f wf_nominal_terms
+
+(* These terms should be well-formed. *)
+
+let () =
+  printf "Checking well-formedness...\n%!";
+  on_wf_nominal_terms (fun t ->
+    assert (wf_term t)
+  )
+
+(* The size computation should succeed. *)
+
+let () =
+  printf "Computing sizes...\n%!";
+  on_wf_nominal_terms (fun t ->
+    ignore (size_term t : int)
+  )
+
+(* [fa] and [occurs] should be consistent with each other. *)
+
+let () =
+  printf "Comparing fa and occurs...\n%!";
+  on_arbitrary_nominal_terms (fun t ->
+    let atoms = fa_term t in
+    Atom.Set.iter (fun a ->
+      if not (occurs_term a t) then begin
+        printf "Atom %a does not occur in term %a" Atom.print a nhprint t
+      end;
+      assert (occurs_term a t); (* slow *)
+    ) atoms
+  )
+
 (* Sample terms. *)
 
 let x =
@@ -48,18 +159,6 @@ let closed_samples = [
 let evaluate f =
   List.iter f samples
 
-(* A non-hygienic term printer. This printer shows the real (internal) identity
-   of atoms, using [Atom.show]. *)
-
-let nhprint oc t =
-  Print.term oc (show_term t)
-
-(* A hygienic term printer. This printer uses [export]. *)
-
-let hprint oc t =
-  (* works for closed terms only, as of now *)
-  Print.term oc (export_term KitExport.empty t)
-
 let () =
   printf "Testing size...\n";
   [
@@ -142,6 +241,7 @@ let () =
   evaluate print_wf;
   print_wf (TApp (id, id))
 
+(*
 let () =
   for _i = 0 to 9 do
     let t = import_term KitImport.empty (generate_raw 15) in
@@ -155,3 +255,4 @@ let () =
     let t = generate_nominal (* atoms: *) 5 (* size: *) 15 in
     printf "generate_nominal() = %a\n%!" nhprint t
   done
+ *)