look up names again
This commit is contained in:
parent
e82e05131c
commit
2e46c8cacf
1 changed files with 6 additions and 1 deletions
|
@ -19,6 +19,11 @@ let rec string_of_term (t: Types.term) =
|
||||||
"(" ^ (string_of_term t1) ^ " " ^ (string_of_term t2) ^ ")"
|
"(" ^ (string_of_term t1) ^ " " ^ (string_of_term t2) ^ ")"
|
||||||
| TmVar(x) -> x
|
| TmVar(x) -> x
|
||||||
|
|
||||||
|
let rec string_of_term_in_ctx ctx tm =
|
||||||
|
match ctx with
|
||||||
|
| [] -> (string_of_term tm)
|
||||||
|
| (n, t)::r -> if t = tm then n else (string_of_term_in_ctx r tm)
|
||||||
|
|
||||||
let rec string_of_ctx (c: Types.context) =
|
let rec string_of_ctx (c: Types.context) =
|
||||||
match c with
|
match c with
|
||||||
| [] -> ""
|
| [] -> ""
|
||||||
|
@ -89,7 +94,7 @@ let _ =
|
||||||
match x with
|
match x with
|
||||||
| Types.Term t ->
|
| Types.Term t ->
|
||||||
let (ctx', r) = eval (ctx, t) in
|
let (ctx', r) = eval (ctx, t) in
|
||||||
print_endline (string_of_term r); flush stdout;
|
print_endline (string_of_term_in_ctx ctx r); flush stdout;
|
||||||
loop ctx'
|
loop ctx'
|
||||||
| Types.Assign (n, t) ->
|
| Types.Assign (n, t) ->
|
||||||
let (ctx', r) = eval (ctx, t) in
|
let (ctx', r) = eval (ctx, t) in
|
||||||
|
|
Loading…
Reference in a new issue