Main.ml 3.05 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 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25
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 =
26
  TApp (delta, copy_term delta)
POTTIER Francois's avatar
POTTIER Francois committed
27 28 29 30 31 32

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

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

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

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

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

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

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

let () =
82
  evaluate print_copy_term
POTTIER Francois's avatar
POTTIER Francois committed
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 108

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

let print_equiv t1 t2 =
  printf "equiv: %a ~ %a = %b\n%!"
    nhprint t1
    nhprint t2
128
    (equiv_term t1 t2)
POTTIER Francois's avatar
POTTIER Francois committed
129 130 131 132 133

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

let print_wf t =
  printf "wf(%a) = %b\n%!"
    nhprint t
147
    (wf_term t)
POTTIER Francois's avatar
POTTIER Francois committed
148 149

let () =
150 151
  evaluate print_wf;
  print_wf (TApp (id, id))
152 153 154 155 156 157

let () =
  for _i = 0 to 9 do
    printf "generate() = %a\n%!"
      hprint (import_term KitImport.empty (generate 10))
  done