<div dir="ltr">I ran into the "v" variable being used internally in the translator problem.<div>Easiest fix would be to have a pass early in the translator that renamed</div><div>all "v"s in definitions to something else. </div><div><br></div><div>Konrad.</div></div><div class="gmail_extra"><br><div class="gmail_quote">On Wed, Feb 1, 2017 at 12:47 PM, Yong Kiam <span dir="ltr"><<a href="mailto:tanyongkiam@gmail.com" target="_blank">tanyongkiam@gmail.com</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div dir="ltr"><div><div>Hi all,<br><br></div>I've been translating the namespace type on env-refactor, but I ran into a name clash problem:<br><br></div>The following term gets anti-quoted out for tDefine:<br><div><br>[ANTIQUOTE<br> ``(NAMESPACE_NAMESPACE_TYPE :<br> (ν -> v -> bool) -><br> (ξ -> v -> bool) -><br> (φ -> v -> bool) -> (ν, ξ, φ) namespace -> v -> bool)<br> (m :ν -> v -> bool) (n :ξ -> v -> bool) <b>(v :φ -> v -> bool)</b><br> (Bind (x_2 :(ξ, φ) alist) (x_1 :(ν, (ν, ξ, φ) namespace) alist))<br> <b>(v :v)</b> ⇔<br> ∃(v1_1 :v) (v1_2 :v).<br> v =<br> Conv<br> (SOME<br> ("Bind",<br> TypeId (Short "namespace_namespace" :(tvarN, tvarN) id)))<br> [v1_1; v1_2] ∧<br> CONTAINER<br> (LIST_TYPE :(ξ # φ -> v -> bool) -> (ξ, φ) alist -> v -> bool)<br> (λ(x :ξ # φ) (v' :v).<br> if MEM x x_2 then<br> CONTAINER<br> (PAIR_TYPE :(ξ -> v -> bool) -><br> (φ -> v -> bool) -> ξ # φ -> v -> bool)<br> (λ(y :ξ) (v :v). if y = FST x then n y v else (ARB :bool))<br> (λ(y :φ) (v' :v).<br> if y = SND x then v y v' else (ARB :bool)) x v'<br> else (ARB :bool)) x_2 v1_1 ∧<br> CONTAINER<br> (LIST_TYPE :(ν # (ν, ξ, φ) namespace -> v -> bool) -><br> (ν, (ν, ξ, φ) namespace) alist -> v -> bool)<br> (λ(x :ν # (ν, ξ, φ) namespace) (v' :v).<br> if MEM x x_1 then<br> CONTAINER<br> (PAIR_TYPE :(ν -> v -> bool) -><br> ((ν, ξ, φ) namespace -> v -> bool) -><br> ν # (ν, ξ, φ) namespace -> v -> bool)<br> (λ(y :ν) (v :v). if y = FST x then m y v else (ARB :bool))<br> (λ(y :(ν, ξ, φ) namespace) (v' :v).<br> if y = SND x then NAMESPACE_NAMESPACE_TYPE m n v y v'<br> else (ARB :bool)) x v'<br> else (ARB :bool)) x_1 v1_2``]<br><br></div><div>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?).<br><br></div><div>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.<br><br></div><div>There are a couple of quickfixes possible, and I was wondering which one seems better:<br><br></div><div>1) Make namespace use some other type variable<br><br></div><div>2) Add unlikely suffixes to autogenerated variable names from type variables<br></div><div><br>3) Make translator check for presence of "v" when picking variable names<br><br></div></div>
<br>______________________________<wbr>_________________<br>
Developers mailing list<br>
<a href="mailto:Developers@cakeml.org">Developers@cakeml.org</a><br>
<a href="https://lists.cakeml.org/listinfo/developers" rel="noreferrer" target="_blank">https://lists.cakeml.org/<wbr>listinfo/developers</a><br>
<br></blockquote></div><br></div>