[isabelle] Isabelle2014-RC0: lift_definition ignores no_code



In Isabelle2014-RC0, lift_definition sometimes forgets that the setup_lifting declaration has been given the (no_code) option. When that happens, I get bogus code equations in the code generator setup which break the value command, because even NBE then complains about sort constraints being violated. Below is an example that works in Isabelle2013-2, but not in Isabelle2014-RC0. Of course, I can manually delete the code equations, but it would be nicer if lift_definition could just stick to what setup_lifting has been told.

theory Scratch imports "~~/src/HOL/Main" begin

typedef ('a, 'b) foo = "{f :: 'a ⇒ 'b. ∀x. f x = undefined}" sorry
setup_lifting (no_code) type_definition_foo

lift_definition make :: "('a ⇒ 'b) ⇒ ('a, 'b) foo"
  is "λg. if ∀x. g x = undefined then g else (λ_. undefined)" sorry

definition bar where "bar = make (λx :: nat. 0 :: nat)"

value "bar"

(* evaluates in Isabelle2013-2 to "make (λu. 0)",
but raises the following error message in Isabelle2014-RC0:

Wellsortedness error
(in code equation bar ≡ make (λx. zero_nat_inst.zero_nat),
with dependency "Pure.dummy_pattern" -> "bar"):
Type nat not of sort enum
No type arity nat :: enum

*)

Best,
Andreas




This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.