Main.ml 11.3 KB
Newer Older
POTTIER Francois's avatar
POTTIER Francois committed
1 2 3
open Printf
open AlphaLib
open Term
4
open TermGenerator
POTTIER Francois's avatar
POTTIER Francois committed
5
open ParallelRed
6 7 8 9

module T =
  Toolbox.Make(Term)

POTTIER Francois's avatar
POTTIER Francois committed
10 11
open T

POTTIER Francois's avatar
POTTIER Francois committed
12 13
let ( ** ) = Atom.Set.union

14 15 16
let subst1 =
  subst_TVar_term1 copy_term

POTTIER Francois's avatar
POTTIER Francois committed
17 18
(* -------------------------------------------------------------------------- *)

19 20 21 22 23 24 25 26 27 28 29 30 31 32
(* [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)

POTTIER Francois's avatar
POTTIER Francois committed
33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56
(* [take n xs] returns the first [n] elements of [xs]. *)

let rec take n xs =
  match n, xs with
  | 0, _
  | _, [] ->
      []
  | _, (x :: xs as input) ->
     let xs' = take (n - 1) xs in
     if xs == xs' then
       input
     else
       x :: xs'

(* [split xs] splits the set of atoms [xs] in two halves. *)

let halve xs =
  let xs = Atom.Set.elements xs in
  let n = List.length xs in
  let xs = take (n/2) xs in
  Atom.Set.of_list xs

(* -------------------------------------------------------------------------- *)

57 58 59 60 61 62 63 64 65 66 67
(* 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)

POTTIER Francois's avatar
POTTIER Francois committed
68
(* -------------------------------------------------------------------------- *)
69

POTTIER Francois's avatar
POTTIER Francois committed
70
(* A test run. *)
POTTIER Francois's avatar
POTTIER Francois committed
71

POTTIER Francois's avatar
POTTIER Francois committed
72 73 74 75 76 77 78 79 80 81 82 83 84
module Run (P : sig

  (* Test parameters. *)

  val number: int
  val size: int
  val atoms: int

end) = struct open P

let () =
  printf "Test run: number = %d, size = %d, atoms = %d.\n%!"
    number size atoms
85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109

(* 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));
110
    assert (guq_term t)
111 112 113 114 115 116 117 118 119 120 121 122 123
  )

(* 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

POTTIER Francois's avatar
POTTIER Francois committed
124
(* Copy them, so as to obtain guq (although non-closed) nominal terms. *)
125

126
let guq_nominal_terms : nominal_term list =
127 128 129
  printf "Copying these terms...\n%!";
  List.map copy_term arbitrary_nominal_terms

130 131
let on_guq_nominal_terms f =
  List.iter f guq_nominal_terms
132

POTTIER Francois's avatar
POTTIER Francois committed
133 134 135 136 137 138
let all_atoms_of_guq_nominal_terms =
  List.fold_left (fun atoms t ->
    atoms ** ba_term t ** fa_term t
  ) Atom.Set.empty guq_nominal_terms


139 140 141 142
(* These terms should be well-formed. *)

let () =
  printf "Checking well-formedness...\n%!";
143 144
  on_guq_nominal_terms (fun t ->
    assert (guq_term t)
145 146
  )

POTTIER Francois's avatar
POTTIER Francois committed
147
(* [size_term] should succeed. *)
148 149

let () =
POTTIER Francois's avatar
POTTIER Francois committed
150 151
  printf "Testing size...\n%!";
  on_arbitrary_nominal_terms (fun t ->
152 153 154
    ignore (size_term t : int)
  )

POTTIER Francois's avatar
POTTIER Francois committed
155 156 157 158 159 160 161 162 163 164 165 166 167 168 169 170 171 172 173 174 175 176 177 178 179 180 181 182
(* [show_term] should succeed. *)

let () =
  printf "Testing show...\n%!";
  on_arbitrary_nominal_terms (fun t ->
    ignore (show_term t : raw_term)
  )

(* On a closed term, [show] is actually hygienic. *)

let () =
  printf "Testing show on closed terms...\n%!";
  on_closed_nominal_terms (fun t ->
    let u : raw_term = show_term t in
    let v : nominal_term = import_term KitImport.empty u in
    assert (equiv_term t v)
  )

(* Round-trip property of [import] and [export] on closed terms. *)

let () =
  printf "Testing import/export round-trip...\n%!";
  on_closed_nominal_terms (fun t ->
    let u : raw_term = export_term KitExport.empty t in
    let v : nominal_term = import_term KitImport.empty u in
    assert (equiv_term t v)
  )

183 184 185
(* [fa] and [occurs] should be consistent with each other. *)

let () =
POTTIER Francois's avatar
POTTIER Francois committed
186
  printf "Comparing fa and closed...\n%!";
187
  on_arbitrary_nominal_terms (fun t ->
POTTIER Francois's avatar
POTTIER Francois committed
188 189
    assert (Atom.Set.is_empty (fa_term t) = closed_term t)
  );
190
  on_guq_nominal_terms (fun t ->
POTTIER Francois's avatar
POTTIER Francois committed
191 192 193 194 195 196 197
    assert (Atom.Set.is_empty (fa_term t) = closed_term t)
  )

(* Our well-formed terms should be disjoint. *)

let () =
  printf "Checking disjointness...\n%!";
198 199
  assert (guq_terms closed_nominal_terms);
  assert (guq_terms guq_nominal_terms)
POTTIER Francois's avatar
POTTIER Francois committed
200 201 202 203 204 205 206 207 208

(* [copy] should be the identity, up to alpha-equivalence. *)

let test_copy t =
  assert (equiv_term t (copy_term t))

let () =
  printf "Testing equiv/copy...\n%!";
  on_arbitrary_nominal_terms test_copy;
209
  on_guq_nominal_terms test_copy;
POTTIER Francois's avatar
POTTIER Francois committed
210 211
  on_closed_nominal_terms test_copy

POTTIER Francois's avatar
POTTIER Francois committed
212 213 214 215 216 217 218
(* Test substitution. *)

let size_of_u = 100

let () =
  printf "Testing substitution...\n%!";
  let (=) = equiv_term in
219
  on_guq_nominal_terms (fun t ->
POTTIER Francois's avatar
POTTIER Francois committed
220 221 222 223 224 225
    (* TEMPORARY should choose randomly and efficiently *)
    match Atom.Set.choose (fa_term t) with
    | exception Not_found ->
        ()
    | x ->
        let u = generate_nominal atoms size_of_u in
226
        let t' = subst1 u x t in
227
        assert (guq_term t');
POTTIER Francois's avatar
POTTIER Francois committed
228 229
        assert (Atom.Set.equal
                  (fa_term t')
POTTIER Francois's avatar
POTTIER Francois committed
230
                  (fa_term u ** Atom.Set.remove x (fa_term t))
POTTIER Francois's avatar
POTTIER Francois committed
231
               );
232
        assert (t' = subst1 u x t);
233
        assert (guq_term (TLambda (x, t)));
234
        (* subst1 u x (TLambda (x, t)) = TLambda (x, t) *)
POTTIER Francois's avatar
POTTIER Francois committed
235 236 237 238
        (* cannot be checked as these are illegal arguments to substitution *)
        begin match t with
        | TVar _ -> assert false
        | TLambda (y, t) ->
239 240
            assert (subst1 u x (TLambda (y, t)) =
                    TLambda (y, subst1 u x t))
POTTIER Francois's avatar
POTTIER Francois committed
241
        | TApp (t1, t2) ->
242 243
            assert (subst1 u x (TApp (t1, t2)) =
                    TApp (subst1 u x t1, subst1 u x t2))
POTTIER Francois's avatar
POTTIER Francois committed
244 245
        end
  );
246 247
  let x = Atom.fresh "x"
  and y = Atom.fresh "y" in
POTTIER Francois's avatar
POTTIER Francois committed
248
  let u = generate_nominal atoms size_of_u in
249 250
  assert (subst1 u x (TVar x) = u);
  assert (subst1 u x (TVar y) = TVar y);
251
  on_guq_nominal_terms (fun t ->
252 253
    assert (subst1 u x t = t);
    assert (subst1 u x t == t) (* note physical equality *)
POTTIER Francois's avatar
POTTIER Francois committed
254 255 256 257 258
  );
  (* Test that [equiv] distinguishes certain terms. *)
  assert (not (TVar x = TVar y));
  assert (not (TLambda (x, TVar x) = TLambda (y, TVar x)));
  assert (not (TVar x = TLambda (x, TVar x)));
POTTIER Francois's avatar
POTTIER Francois committed
259 260 261 262 263 264
  assert (not (TLambda (x, TLambda (y, TVar x)) = TLambda (x, TLambda (y, TVar y))));
  (* Negative test of [avoids] and [guq]. *)
  assert (not (avoids_term (Atom.Set.singleton x) (TLambda (x, TVar y))));
  assert (not (avoids_term (Atom.Set.empty) (TLambda (x, TLambda (x, TVar y)))));
  assert (not (guq_term (TApp (TLambda (x, TVar y), TLambda (x, TVar y)))));
  ()
POTTIER Francois's avatar
POTTIER Francois committed
265

266 267 268 269 270 271 272
(* [fa] and [ba] should be consistent with each other. *)

let () =
  printf "Checking fa and ba are consistent...\n%!";
  on_guq_nominal_terms (fun t ->
    let ba = ba_term t
    and fa = fa_term t in
POTTIER Francois's avatar
POTTIER Francois committed
273 274 275 276 277 278 279 280 281 282 283 284 285 286 287 288 289 290
    assert (Atom.Set.disjoint ba fa);
    assert (avoids_term fa t)
  )

(* Test [avoid] and [avoids]. Must use guq terms because [avoids] requires
   no shadowing. *)

let () =
  printf "Computing all atoms of our guq terms...\n%!";
  let some_atoms = halve (halve (all_atoms_of_guq_nominal_terms)) in
  printf "Testing avoids on %d of %d atoms...\n%!"
    (Atom.Set.cardinal some_atoms)
    (Atom.Set.cardinal all_atoms_of_guq_nominal_terms)
  ;
  on_guq_nominal_terms (fun t ->
    let t' = avoid_term some_atoms t in
    assert (equiv_term t t');
    assert (avoids_term some_atoms t')
291 292
  )

POTTIER Francois's avatar
POTTIER Francois committed
293 294 295 296 297 298
(* [fa] and [occurs] should be consistent with each other. *)

let () =
  printf "Comparing fa and occurs... (quadratic)\n%!";
  on_arbitrary_nominal_terms (fun t ->
    let fa = fa_term t in
299 300
    Atom.Set.iter (fun a ->
      assert (occurs_term a t); (* slow *)
POTTIER Francois's avatar
POTTIER Francois committed
301 302
    ) fa
  );
303
  on_guq_nominal_terms (fun t ->
POTTIER Francois's avatar
POTTIER Francois committed
304 305 306 307 308 309
    let ba = ba_term t in
    let fa = fa_term t in
    assert (Atom.Set.is_empty (Atom.Set.inter ba fa));
    Atom.Set.iter (fun a ->
      assert (not (occurs_term a t)) (* slow *)
    ) ba
310 311
  )

POTTIER Francois's avatar
POTTIER Francois committed
312 313 314 315 316 317 318 319 320 321 322 323 324 325 326 327 328
end

(* -------------------------------------------------------------------------- *)

(* Run tests with increasing parameter sizes. *)

let rec run number size atoms =
  if size <= 3000 then
    let module R = Run(struct
      let number = number
      let size = size
      let atoms = atoms
    end) in
    run number (3 * size) (2 * atoms)

let () =
  run 1000 1 1
POTTIER Francois's avatar
POTTIER Francois committed
329

POTTIER Francois's avatar
POTTIER Francois committed
330 331 332
(* Sample terms. *)

let x =
333
  Atom.fresh "x"
POTTIER Francois's avatar
POTTIER Francois committed
334 335

let y =
336
  Atom.fresh "y"
POTTIER Francois's avatar
POTTIER Francois committed
337 338 339 340 341 342 343 344 345 346 347

let id =
  TLambda (x, TVar x)

let delta_body =
  TApp (TVar x, TVar x)

let delta =
  TLambda (x, delta_body)

let omega =
348
  TApp (delta, copy_term delta)
POTTIER Francois's avatar
POTTIER Francois committed
349 350 351 352 353 354

let samples = [
    TVar y;
    id;
    TApp (id, TVar y);
    TApp (id, TVar x);
355
    TApp (id, copy_term id);
POTTIER Francois's avatar
POTTIER Francois committed
356 357
    delta;
    omega;
358 359
    import_term KitImport.empty (TLambda ("x", TVar "x"));
    import_term KitImport.empty (TLambda ("z", TLambda ("z", TVar "z")));
POTTIER Francois's avatar
POTTIER Francois committed
360 361 362 363
  ]

let closed_samples = [
    id;
364
    TApp (id, copy_term id);
POTTIER Francois's avatar
POTTIER Francois committed
365 366
    delta;
    omega;
367
    import_term KitImport.empty (TLambda ("z", TLambda ("z", TVar "z")));
POTTIER Francois's avatar
POTTIER Francois committed
368 369 370 371 372 373 374 375 376 377 378
  ]

let evaluate f =
  List.iter f samples

let () =
  printf "Testing size...\n";
  [
    TVar y, 1;
    id, 2;
    TApp (id, TVar y), 4;
379
    TApp (id, copy_term id), 5;
POTTIER Francois's avatar
POTTIER Francois committed
380 381 382
    delta, 4;
    omega, 9;
  ] |> List.iter (fun (t, i) ->
383
    assert (size_term t = i)
POTTIER Francois's avatar
POTTIER Francois committed
384 385
  )

386 387
let print_copy_term t =
  printf "copy_term(%a) = %a\n%!"
POTTIER Francois's avatar
POTTIER Francois committed
388
    nhprint t
389
    nhprint (copy_term t)
POTTIER Francois's avatar
POTTIER Francois committed
390 391

let () =
392
  evaluate print_copy_term
POTTIER Francois's avatar
POTTIER Francois committed
393 394 395 396 397 398 399 400 401 402 403 404

let print_export t =
  printf "export(%a) = %a\n%!"
    nhprint t
    hprint t

let () =
  List.iter print_export closed_samples

let print_fa t =
  printf "fa(%a) = %a\n%!"
    nhprint t
POTTIER Francois's avatar
POTTIER Francois committed
405
    Atom.Set.print (fa_term t)
POTTIER Francois's avatar
POTTIER Francois committed
406 407 408 409 410

let () =
  evaluate print_fa

let print_subst1 u x t =
411
  let t' = subst1 u x t in
POTTIER Francois's avatar
POTTIER Francois committed
412 413 414 415 416 417 418 419 420 421 422
  printf "substituting %a for %a in %a = ...\n  %a\n%s\n%!"
    nhprint u
    Atom.print x
    nhprint t
    nhprint t'
    (if t == t' then "(physically equal)" else "(physically distinct)")

let () =
  print_subst1 (TVar y) x (TVar x);
  print_subst1 (TVar y) x (TVar y);
  print_subst1 delta x delta_body;
423
  print_subst1 (copy_term delta) x (copy_term delta);
POTTIER Francois's avatar
POTTIER Francois committed
424 425 426 427 428 429
  ()

let print_equiv t1 t2 =
  printf "equiv: %a ~ %a = %b\n%!"
    nhprint t1
    nhprint t2
430
    (equiv_term t1 t2)
POTTIER Francois's avatar
POTTIER Francois committed
431 432 433 434 435

let () =
  print_equiv id id;
  print_equiv id (TVar x);
  print_equiv (TVar x) (TVar y);
436 437
  print_equiv delta (copy_term delta);
  print_equiv omega (copy_term omega);
POTTIER Francois's avatar
POTTIER Francois committed
438 439 440
  print_equiv (TLambda (x, TVar x)) (TLambda (y, TVar y));
  print_equiv (TLambda (x, TVar x)) (TLambda (y, TVar x));
  print_equiv
441 442
    (import_term KitImport.empty (TLambda ("z", TLambda ("z", TVar "z"))))
    (import_term KitImport.empty (TLambda ("z", TLambda ("y", TVar "z"))))
POTTIER Francois's avatar
POTTIER Francois committed
443 444 445
  ;
  ()

POTTIER Francois's avatar
POTTIER Francois committed
446 447
let print_guq t =
  printf "guq(%a) = %b\n%!"
POTTIER Francois's avatar
POTTIER Francois committed
448
    nhprint t
449
    (guq_term t)
POTTIER Francois's avatar
POTTIER Francois committed
450 451

let () =
POTTIER Francois's avatar
POTTIER Francois committed
452 453
  evaluate print_guq;
  print_guq (TApp (id, id))
454

455
(*
456
let () =
457
  for _i = 0 to 9 do
458 459
    let t = import_term KitImport.empty (generate_raw 15) in
    printf "generate_raw() = %a\n%!" hprint t;
POTTIER Francois's avatar
POTTIER Francois committed
460 461
    assert (closed_term t);
    assert (Atom.Set.is_empty (fa_term t));
462
  done
463 464 465 466 467 468

let () =
  for _i = 0 to 9 do
    let t = generate_nominal (* atoms: *) 5 (* size: *) 15 in
    printf "generate_nominal() = %a\n%!" nhprint t
  done
469
 *)