test03.ml 1.51 KB
Newer Older
POTTIER Francois's avatar
POTTIER Francois committed
1 2 3 4 5
type ('var, 'binder) term =
  | TVar of 'var
  | TAbs of 'binder * ('var, 'binder) term
  | TApp of ('var, 'binder) term * ('var, 'binder) term
[@@deriving
6 7
     visitors { variety = "iter" },
     visitors { variety = "map" },
POTTIER Francois's avatar
POTTIER Francois committed
8 9
     visitors { variety = "reduce" },
     visitors { variety = "endo" },
10
     visitors { variety = "iter2" },
POTTIER Francois's avatar
POTTIER Francois committed
11 12
     visitors { variety = "map2" },
     visitors { variety = "reduce2" }
POTTIER Francois's avatar
POTTIER Francois committed
13 14 15 16 17 18 19
]

(* Nominal. *)

module StringSet = Set.Make(String)

let iter = object(self)
20
  inherit [_] iter
POTTIER Francois's avatar
POTTIER Francois committed
21
  (* Descending methods for local types. *)
22
  method! visit_TAbs env x t =
POTTIER Francois's avatar
POTTIER Francois committed
23 24 25
    let env = StringSet.add x env in
    self#visit_term env t
  (* Descending methods for nonlocal types. *)
26
  method visit_'binder _env _x = ()
POTTIER Francois's avatar
POTTIER Francois committed
27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43
  method visit_'var env x =
    if StringSet.mem x env then
      Printf.printf "%s is a bound variable.\n%!" x
    else
      Printf.printf "%s is a free variable.\n%!" x

end

let t : (_, _) term =
  TAbs ("x", TApp (TVar "x", TVar "y"))

let () =
  iter#visit_term StringSet.empty t

(* De Bruijn. *)

let iter = object(self)
44
  inherit [_] iter
POTTIER Francois's avatar
POTTIER Francois committed
45
  (* Descending methods for local types. *)
46
  method! visit_TAbs env _x t =
POTTIER Francois's avatar
POTTIER Francois committed
47 48 49
    let env = 1 + env in
    self#visit_term env t
  (* Descending methods for nonlocal types. *)
50
  method visit_'binder _env _x = ()
POTTIER Francois's avatar
POTTIER Francois committed
51 52 53 54 55 56 57 58 59 60 61 62 63
  method visit_'var env x =
    if x < env then
      Printf.printf "%d is a bound variable.\n%!" x
    else
      Printf.printf "%d is a free variable.\n%!" x

end

let t : (_, _) term =
  TAbs ((), TApp (TVar 0, TVar 1))

let () =
  iter#visit_term 0 t