diff options
author | Son Ho | 2021-11-30 20:59:30 +0100 |
---|---|---|
committer | Son Ho | 2021-11-30 20:59:30 +0100 |
commit | 7963e3ee84090b96308eebc68ee20532ea85c532 (patch) | |
tree | 566ddf1e10b74d9cfa4111869369d9d1649e35fe /src/Print.ml | |
parent | 4caa42db826999e4df74e2e3abf80f2b4c2650fa (diff) |
Introduce [binder] and use them in place of [var] in the environments
Diffstat (limited to 'src/Print.ml')
-rw-r--r-- | src/Print.ml | 11 |
1 files changed, 8 insertions, 3 deletions
diff --git a/src/Print.ml b/src/Print.ml index bb172d5f..911de5e3 100644 --- a/src/Print.ml +++ b/src/Print.ml @@ -400,11 +400,16 @@ module PV = Values (* local module *) (** Pretty-printing for contexts *) module Contexts = struct + let binder_to_string (bv : C.binder) : string = + match bv.name with + | None -> PV.var_id_to_string bv.index + | Some name -> name + let env_value_to_string (fmt : PV.value_formatter) (ev : C.env_value) : string = match ev with | Var (var, tv) -> - PV.var_to_string var ^ " -> " ^ PV.typed_value_to_string fmt tv ^ " ;" + binder_to_string var ^ " -> " ^ PV.typed_value_to_string fmt tv ^ " ;" | Abs abs -> PV.abs_to_string fmt abs | Frame -> failwith "Can't print a Frame element" @@ -456,8 +461,8 @@ module Contexts = struct type_ctx_to_adt_variant_to_string_fun ctx.type_context in let var_id_to_string vid = - let var = C.ctx_lookup_var ctx vid in - PV.var_to_string var + let bv = C.ctx_lookup_binder ctx vid in + binder_to_string bv in let adt_field_names = type_ctx_to_adt_field_names_fun ctx.C.type_context in { |