58 lines
1.5 KiB
OCaml
58 lines
1.5 KiB
OCaml
(*
|
|
https://www.cis.upenn.edu/~bcpierce/tapl/checkers/untyped/
|
|
https://web.archive.org/web/20210423155718/https://www.cis.upenn.edu/~bcpierce/tapl/checkers/
|
|
*)
|
|
|
|
(* ** Compilation
|
|
|
|
ocamlc in.sml -o out.out
|
|
*)
|
|
|
|
type info = FI of string * int * int | UNKNOWN
|
|
type binding = NameBind
|
|
type context = (string * binding) list
|
|
|
|
let rec isnamebound ctx x =
|
|
match ctx with
|
|
[] -> false
|
|
| (y,_)::rest ->
|
|
if y=x then true
|
|
else isnamebound rest x
|
|
|
|
let rec pickfreshname ctx x =
|
|
if isnamebound ctx x then pickfreshname ctx (x^"'")
|
|
else ((x,NameBind)::ctx), x
|
|
|
|
|
|
|
|
(* Bare bones definition of [term]
|
|
|
|
type term = Var of int (* de-Bruijn index *)
|
|
| Abs of term
|
|
| App of term * term
|
|
|
|
But we are using some annotations to make debugging easier.
|
|
|
|
- info: File position where term was found, so errors can point out where the error occurred.
|
|
- int: For [Var] nodes. Total length of the context in which the variable is occuring. For a consistency check.
|
|
- string: For [Abs] nodes. To replace de-Bruijn index with a variable name similar to what was used by user.
|
|
*)
|
|
|
|
type term = Var of info * int * int
|
|
| Abs of info * term * string
|
|
| App of info * term * term
|
|
|
|
|
|
(* Recursive function to print terms *)
|
|
let rec printTerm ctxt t = match t with
|
|
Abs(inf, trm, strng) ->
|
|
let (ctx', trm') = pickfreshname ctx x
|
|
in
|
|
print_string "(lambda ";
|
|
(* ... *)
|
|
| App(inf, t1, t2) ->
|
|
|
|
|
|
(* print_string "Hello world!" *)
|
|
|