[CakeML-dev] Bad names for translator

[Yong Kiam]

Hi all,

I've been translating the namespace type on env-refactor, but I ran into a
name clash problem:

The following term gets anti-quoted out for tDefine:

[ANTIQUOTE
      ``(NAMESPACE_NAMESPACE_TYPE :
    (ν -> v -> bool) ->
    (ξ -> v -> bool) ->
    (φ -> v -> bool) -> (ν, ξ, φ) namespace -> v -> bool)
    (m :ν -> v -> bool) (n :ξ -> v -> bool) *(v :φ -> v -> bool)*
    (Bind (x_2 :(ξ, φ) alist) (x_1 :(ν, (ν, ξ, φ) namespace) alist))
    *(v :v)* ⇔
  ∃(v1_1 :v) (v1_2 :v).
    v =
    Conv
      (SOME
         ("Bind",
          TypeId (Short "namespace_namespace" :(tvarN, tvarN) id)))
      [v1_1; v1_2] ∧
    CONTAINER
      (LIST_TYPE :(ξ # φ -> v -> bool) -> (ξ, φ) alist -> v -> bool)
      (λ(x :ξ # φ) (v' :v).
         if MEM x x_2 then
           CONTAINER
             (PAIR_TYPE :(ξ -> v -> bool) ->
                         (φ -> v -> bool) -> ξ # φ -> v -> bool)
             (λ(y :ξ) (v :v). if y = FST x then n y v else (ARB :bool))
             (λ(y :φ) (v' :v).
                if y = SND x then v y v' else (ARB :bool)) x v'
         else (ARB :bool)) x_2 v1_1 ∧
    CONTAINER
      (LIST_TYPE :(ν # (ν, ξ, φ) namespace -> v -> bool) ->
                  (ν, (ν, ξ, φ) namespace) alist -> v -> bool)
      (λ(x :ν # (ν, ξ, φ) namespace) (v' :v).
         if MEM x x_1 then
           CONTAINER
             (PAIR_TYPE :(ν -> v -> bool) ->
                         ((ν, ξ, φ) namespace -> v -> bool) ->
                         ν # (ν, ξ, φ) namespace -> v -> bool)
             (λ(y :ν) (v :v). if y = FST x then m y v else (ARB :bool))
             (λ(y :(ν, ξ, φ) namespace) (v' :v).
                if y = SND x then NAMESPACE_NAMESPACE_TYPE m n v y v'
                else (ARB :bool)) x v'
         else (ARB :bool)) x_1 v1_2``]

However, it has two instances of v at different types (in bold), and it
doesn't parse back in as a term (probably HOL decided to use the later
instance for type checking?).

The problem seems to be that the namespace is defined with 'v as one of its
type variables and "v" is used all over the translator.

There are a couple of quickfixes possible, and I was wondering which one
seems better:

1) Make namespace use some other type variable

2) Add unlikely suffixes to autogenerated variable names from type variables

3) Make translator check for presence of "v" when picking variable names
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://lists.cakeml.org/pipermail/developers/attachments/20170201/eab95644/attachment.html>