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

module T =
  Toolbox.Make(Term)

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

11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37
(* [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. *)

POTTIER Francois's avatar
POTTIER Francois committed
38 39
(* TEMPORARY test with small parameters first, then increase. *)

40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67
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));
68
    assert (guq_term t)
69 70 71 72 73 74 75 76 77 78 79 80 81 82 83
  )

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

84
let guq_nominal_terms : nominal_term list =
85 86 87
  printf "Copying these terms...\n%!";
  List.map copy_term arbitrary_nominal_terms

88 89
let on_guq_nominal_terms f =
  List.iter f guq_nominal_terms
90 91 92 93 94

(* These terms should be well-formed. *)

let () =
  printf "Checking well-formedness...\n%!";
95 96
  on_guq_nominal_terms (fun t ->
    assert (guq_term t)
97 98
  )

POTTIER Francois's avatar
POTTIER Francois committed
99
(* [size_term] should succeed. *)
100 101

let () =
POTTIER Francois's avatar
POTTIER Francois committed
102 103
  printf "Testing size...\n%!";
  on_arbitrary_nominal_terms (fun t ->
104 105 106
    ignore (size_term t : int)
  )

POTTIER Francois's avatar
POTTIER Francois committed
107 108 109 110 111 112 113 114 115 116 117 118 119 120 121 122 123 124 125 126 127 128 129 130 131 132 133 134
(* [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)
  )

135 136 137
(* [fa] and [occurs] should be consistent with each other. *)

let () =
POTTIER Francois's avatar
POTTIER Francois committed
138
  printf "Comparing fa and closed...\n%!";
139
  on_arbitrary_nominal_terms (fun t ->
POTTIER Francois's avatar
POTTIER Francois committed
140 141
    assert (Atom.Set.is_empty (fa_term t) = closed_term t)
  );
142
  on_guq_nominal_terms (fun t ->
POTTIER Francois's avatar
POTTIER Francois committed
143 144 145 146 147 148 149
    assert (Atom.Set.is_empty (fa_term t) = closed_term t)
  )

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

let () =
  printf "Checking disjointness...\n%!";
150 151
  assert (guq_terms closed_nominal_terms);
  assert (guq_terms guq_nominal_terms)
POTTIER Francois's avatar
POTTIER Francois committed
152 153 154 155 156 157 158 159 160

(* [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;
161
  on_guq_nominal_terms test_copy;
POTTIER Francois's avatar
POTTIER Francois committed
162 163
  on_closed_nominal_terms test_copy

POTTIER Francois's avatar
POTTIER Francois committed
164 165 166 167 168 169 170
(* Test substitution. *)

let size_of_u = 100

let () =
  printf "Testing substitution...\n%!";
  let (=) = equiv_term in
171
  on_guq_nominal_terms (fun t ->
POTTIER Francois's avatar
POTTIER Francois committed
172 173 174 175 176 177 178
    (* 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
        let t' = subst_term_term1 u x t in
179
        assert (guq_term t');
POTTIER Francois's avatar
POTTIER Francois committed
180 181 182 183 184
        assert (Atom.Set.equal
                  (fa_term t')
                  (Atom.Set.union (fa_term u) (Atom.Set.remove x (fa_term t)))
               );
        assert (t' = subst_term_term1 u x t);
185
        assert (guq_term (TLambda (x, t)));
POTTIER Francois's avatar
POTTIER Francois committed
186 187 188 189 190 191 192 193 194 195 196 197 198 199 200 201 202
        (* subst_term_term1 u x (TLambda (x, t)) = TLambda (x, t) *)
        (* cannot be checked as these are illegal arguments to substitution *)
        begin match t with
        | TVar _ -> assert false
        | TLambda (y, t) ->
            assert (subst_term_term1 u x (TLambda (y, t)) =
                    TLambda (y, subst_term_term1 u x t))
        | TApp (t1, t2) ->
            assert (subst_term_term1 u x (TApp (t1, t2)) =
                    TApp (subst_term_term1 u x t1, subst_term_term1 u x t2))
        end
  );
  let x = Atom.freshh "x"
  and y = Atom.freshh "y" in
  let u = generate_nominal atoms size_of_u in
  assert (subst_term_term1 u x (TVar x) = u);
  assert (subst_term_term1 u x (TVar y) = TVar y);
203
  on_guq_nominal_terms (fun t ->
POTTIER Francois's avatar
POTTIER Francois committed
204 205 206 207 208 209 210 211 212
    assert (subst_term_term1 u x t = t);
    assert (subst_term_term1 u x t == t) (* note physical equality *)
  );
  (* 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)));
  assert (not (TLambda (x, TLambda (y, TVar x)) = TLambda (x, TLambda (y, TVar y))))

213 214 215 216 217 218 219 220 221 222
(* [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
    assert (Atom.Set.disjoint ba fa)
  )

POTTIER Francois's avatar
POTTIER Francois committed
223 224 225 226 227 228
(* [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
229 230
    Atom.Set.iter (fun a ->
      assert (occurs_term a t); (* slow *)
POTTIER Francois's avatar
POTTIER Francois committed
231 232
    ) fa
  );
233
  on_guq_nominal_terms (fun t ->
POTTIER Francois's avatar
POTTIER Francois committed
234 235 236 237 238 239
    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
240 241
  )

POTTIER Francois's avatar
POTTIER Francois committed
242 243
(* TEMPORARY cleanup beyond this line *)

POTTIER Francois's avatar
POTTIER Francois committed
244 245 246 247 248 249 250 251 252 253 254 255 256 257 258 259 260 261
(* Sample terms. *)

let x =
  Atom.freshh "x"

let y =
  Atom.freshh "y"

let id =
  TLambda (x, TVar x)

let delta_body =
  TApp (TVar x, TVar x)

let delta =
  TLambda (x, delta_body)

let omega =
262
  TApp (delta, copy_term delta)
POTTIER Francois's avatar
POTTIER Francois committed
263 264 265 266 267 268

let samples = [
    TVar y;
    id;
    TApp (id, TVar y);
    TApp (id, TVar x);
269
    TApp (id, copy_term id);
POTTIER Francois's avatar
POTTIER Francois committed
270 271
    delta;
    omega;
272 273
    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
274 275 276 277
  ]

let closed_samples = [
    id;
278
    TApp (id, copy_term id);
POTTIER Francois's avatar
POTTIER Francois committed
279 280
    delta;
    omega;
281
    import_term KitImport.empty (TLambda ("z", TLambda ("z", TVar "z")));
POTTIER Francois's avatar
POTTIER Francois committed
282 283 284 285 286 287 288 289 290 291 292
  ]

let evaluate f =
  List.iter f samples

let () =
  printf "Testing size...\n";
  [
    TVar y, 1;
    id, 2;
    TApp (id, TVar y), 4;
293
    TApp (id, copy_term id), 5;
POTTIER Francois's avatar
POTTIER Francois committed
294 295 296
    delta, 4;
    omega, 9;
  ] |> List.iter (fun (t, i) ->
297
    assert (size_term t = i)
POTTIER Francois's avatar
POTTIER Francois committed
298 299
  )

300 301
let print_copy_term t =
  printf "copy_term(%a) = %a\n%!"
POTTIER Francois's avatar
POTTIER Francois committed
302
    nhprint t
303
    nhprint (copy_term t)
POTTIER Francois's avatar
POTTIER Francois committed
304 305

let () =
306
  evaluate print_copy_term
POTTIER Francois's avatar
POTTIER Francois committed
307 308 309 310 311 312 313 314 315 316 317 318

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
319
    Atom.Set.print (fa_term t)
POTTIER Francois's avatar
POTTIER Francois committed
320 321 322 323 324

let () =
  evaluate print_fa

let print_subst1 u x t =
325
  let t' = subst_term_term1 u x t in
POTTIER Francois's avatar
POTTIER Francois committed
326 327 328 329 330 331 332 333 334 335 336
  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;
337
  print_subst1 (copy_term delta) x (copy_term delta);
POTTIER Francois's avatar
POTTIER Francois committed
338 339 340 341 342 343
  ()

let print_equiv t1 t2 =
  printf "equiv: %a ~ %a = %b\n%!"
    nhprint t1
    nhprint t2
344
    (equiv_term t1 t2)
POTTIER Francois's avatar
POTTIER Francois committed
345 346 347 348 349

let () =
  print_equiv id id;
  print_equiv id (TVar x);
  print_equiv (TVar x) (TVar y);
350 351
  print_equiv delta (copy_term delta);
  print_equiv omega (copy_term omega);
POTTIER Francois's avatar
POTTIER Francois committed
352 353 354
  print_equiv (TLambda (x, TVar x)) (TLambda (y, TVar y));
  print_equiv (TLambda (x, TVar x)) (TLambda (y, TVar x));
  print_equiv
355 356
    (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
357 358 359 360 361 362
  ;
  ()

let print_wf t =
  printf "wf(%a) = %b\n%!"
    nhprint t
363
    (guq_term t)
POTTIER Francois's avatar
POTTIER Francois committed
364 365

let () =
366 367
  evaluate print_wf;
  print_wf (TApp (id, id))
368

369
(*
370
let () =
371
  for _i = 0 to 9 do
372 373
    let t = import_term KitImport.empty (generate_raw 15) in
    printf "generate_raw() = %a\n%!" hprint t;
POTTIER Francois's avatar
POTTIER Francois committed
374 375
    assert (closed_term t);
    assert (Atom.Set.is_empty (fa_term t));
376
  done
377 378 379 380 381 382

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