[CakeML-dev] Bad names for translator

[Konrad Slind]

I ran into the "v" variable being used internally in the translator problem.
Easiest fix would be to have a pass early in the translator that renamed
all "v"s in definitions to something else.

Konrad.

On Wed, Feb 1, 2017 at 12:47 PM, Yong Kiam <tanyongkiam at gmail.com> wrote:

> 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
>
>
> _______________________________________________
> Developers mailing list
> Developers at cakeml.org
> https://lists.cakeml.org/listinfo/developers
>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://lists.cakeml.org/pipermail/developers/attachments/20170201/c0816f57/attachment.html>