Main.ml 2.9 KB
Newer Older
POTTIER Francois's avatar
POTTIER Francois committed
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24
open Printf
open AlphaLib
open Term
module T = Toolbox.Make(Term)
open T

(* 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 =
25
  TApp (delta, copy_term delta)
POTTIER Francois's avatar
POTTIER Francois committed
26 27 28 29 30 31

let samples = [
    TVar y;
    id;
    TApp (id, TVar y);
    TApp (id, TVar x);
32
    TApp (id, copy_term id);
POTTIER Francois's avatar
POTTIER Francois committed
33 34
    delta;
    omega;
35 36
    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
37 38 39 40
  ]

let closed_samples = [
    id;
41
    TApp (id, copy_term id);
POTTIER Francois's avatar
POTTIER Francois committed
42 43
    delta;
    omega;
44
    import_term KitImport.empty (TLambda ("z", TLambda ("z", TVar "z")));
POTTIER Francois's avatar
POTTIER Francois committed
45 46 47 48 49 50 51 52 53
  ]

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 =
54
  Print.term oc (show_term t)
POTTIER Francois's avatar
POTTIER Francois committed
55 56 57 58 59

(* A hygienic term printer. This printer uses [export]. *)

let hprint oc t =
  (* works for closed terms only, as of now *)
60
  Print.term oc (export_term KitExport.empty t)
POTTIER Francois's avatar
POTTIER Francois committed
61 62 63 64 65 66 67

let () =
  printf "Testing size...\n";
  [
    TVar y, 1;
    id, 2;
    TApp (id, TVar y), 4;
68
    TApp (id, copy_term id), 5;
POTTIER Francois's avatar
POTTIER Francois committed
69 70 71
    delta, 4;
    omega, 9;
  ] |> List.iter (fun (t, i) ->
72
    assert (size_term t = i)
POTTIER Francois's avatar
POTTIER Francois committed
73 74
  )

75 76
let print_copy_term t =
  printf "copy_term(%a) = %a\n%!"
POTTIER Francois's avatar
POTTIER Francois committed
77
    nhprint t
78
    nhprint (copy_term t)
POTTIER Francois's avatar
POTTIER Francois committed
79 80

let () =
81
  evaluate print_copy_term
POTTIER Francois's avatar
POTTIER Francois committed
82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107

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
    Atom.Set.print (fa t)

let () =
  evaluate print_fa

let print_fa' t =
  printf "fa'(%a) = %a\n%!"
    nhprint t
    Atom.Set.print (fa' t)

let () =
  evaluate print_fa'

let print_subst1 u x t =
108
  let t' = subst_term_term1 u x t in
POTTIER Francois's avatar
POTTIER Francois committed
109 110 111 112 113 114 115 116 117 118 119
  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;
120
  print_subst1 (copy_term delta) x (copy_term delta);
POTTIER Francois's avatar
POTTIER Francois committed
121 122 123 124 125 126 127 128 129 130 131 132
  ()

let print_equiv t1 t2 =
  printf "equiv: %a ~ %a = %b\n%!"
    nhprint t1
    nhprint t2
    (equiv t1 t2)

let () =
  print_equiv id id;
  print_equiv id (TVar x);
  print_equiv (TVar x) (TVar y);
133 134
  print_equiv delta (copy_term delta);
  print_equiv omega (copy_term omega);
POTTIER Francois's avatar
POTTIER Francois committed
135 136 137
  print_equiv (TLambda (x, TVar x)) (TLambda (y, TVar y));
  print_equiv (TLambda (x, TVar x)) (TLambda (y, TVar x));
  print_equiv
138 139
    (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
140 141 142 143 144 145 146 147 148 149
  ;
  ()

let print_wf t =
  printf "wf(%a) = %b\n%!"
    nhprint t
    (try wf t; true with IllFormed _ -> false)

let () =
  evaluate print_wf