[isabelle-dev] Problems with Code-Generator
Dear all,
Chris and I have recently ported our libraries IsaFoR and TermFun to the
development version which worked nicely, except for one issue, which arises
when we want to import external proofs into Isabelle.
The below theory compiles in Isabelle 2013 without problems.
The problem is that no matter, how we adjust the imports / code_reflect
settings,
we get different errors with the repository version (6a7ee03902c3) when
invoking the apply eval statement in the last proof:
importing ~~/src/HOL/Library/Code_Target_Numeral, no code_reflect:
works, but not desired
importing ~~/src/HOL/Library/Code_Target_Numeral, code_reflect mentions nat,
but not int (as it worked in 2013):
Error: Type error in function application.
Function: Checker.checker : Checker.inta - Checker.proof - bool
Argument: (Int_of_integer (25 : IntInf.int)) : inta
Reason: Can't unify Checker.inta with inta (Different type constructors)
importing ~~/src/HOL/Library/Code_Target_Numeral, code_reflect mentions both
int and nat:
previous error disappears, but Abstraction violation: constant
Code_Target_Nat.Nat in last apply eval
importing ~~/src/HOL/Library/Code_Target_Numeral, code_reflect mentions only
int, but not nat:
same as before
trying to also load Code_Binary_Nat also did not help.
Any feedback is welcome.
Cheers,
René
theory Test_Import
imports Main
~~/src/HOL/Library/Code_Char
(* in repository: ~~/src/HOL/Library/Code_Target_Numeral *)
(* in 2013: *)
~~/src/HOL/Library/Code_Integer
~~/src/HOL/Library/Code_Natural
begin
definition parse_digit :: char = nat where
parse_digit c = (
if c = CHR ''0'' then 0 else
if c = CHR ''1'' then 1 else
if c = CHR ''2'' then 2 else
if c = CHR ''3'' then 3 else
if c = CHR ''4'' then 4 else
if c = CHR ''5'' then 5 else
if c = CHR ''6'' then 6 else
if c = CHR ''7'' then 7 else
if c = CHR ''8'' then 8 else 9)
datatype proof = N nat | I int
definition parse_proof :: string = proof where
parse_proof input = (case input of
t # d # _ =
if t = CHR ''n'' then N (parse_digit d)
else I (of_nat (parse_digit d)))
definition parse_proof_term :: string = Code_Evaluation.term where
parse_proof_term input == Code_Evaluation.term_of (parse_proof input)
ML {*
structure Parser =
struct
val parse = String.explode # @{code parse_proof_term}
end
*}
fun checker :: int = proof = bool where
checker n (N i) = (of_nat i * of_nat i = n)
| checker n (I i) = (i * i = n)
lemma checker_imp_square: checker n p ⟹ ? x. x * x = n
by (cases p, auto)
(* precompilation of checker-code, so that it does not need to
be recompiled on every invokation of eval later on,
strangely, in 2013 only nat must be registered as datatype, but not int *)
code_reflect Checker
datatypes (* in repo: int = _ and *) nat = _ and proof = _
functions checker Trueprop
declare checker_def[code del]
setup {*
let
fun import_proof_tac ctxt input i =
let
val thy = Proof_Context.theory_of ctxt
val prf = cterm_of thy (Parser.parse input)
in
rtac @{thm checker_imp_square} i
THEN PRIMITIVE (Drule.instantiate' [] [SOME prf])
end
in
Method.setup @{binding import_proof}
(Scan.lift Parse.string (fn input = fn ctxt = SIMPLE_METHOD'
(import_proof_tac ctxt input)))
instantiates a proof via ML, usually, the string would be some file
content
end
*}
lemma ? x :: int. x * x = 25
apply (import_proof i5)
apply eval
done
lemma ? x :: int. x * x = 25
apply (import_proof n5)
apply eval
(*
On repository version:
Abstraction violation:
constant Code_Target_Nat.Nat
*)
done
end
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Problems with Code-Generator
Hi René,
Florian has reworked the setup for target language numerals. I can at least explain why
you run into the error and provide a workaround.
Code_Target_Nat implements the type nat as an abstract type (code abstype) with
constructor Code_Target_Nat.Nat, i.e., Code_Target_Nat.Nat must not appear in any equation
of the code generator. Unfortunately, this declaration also sets up the term_of function
for type nat to produce terms with this constructor. In the second example, your
import_proof method uses the term_of function to get a term for the given proof (and the
number contained in the proof) and introduces along with this number into the goal state.
As term_of uses the forbidden constructor Code_Target_Nat.Nat, when you then apply eval,
the code generator complains that the abstract constructor is part of the goal state.
The simplest solution is to introduce a new constructor for which you can prove a code
equation. For example, the following defines a constructor Nat2 and redefines term_of for
naturals to use Nat2. When you add it to your theory before declaring the parser
structure, the second example works, too (tested with Isabelle 2b68f4109075). You then
also have to reflect both nat and int as datatypes.
definition Nat2 :: integer = nat
where [code del]: Nat2 = Nat
lemma [code abstract]: integer_of_nat (Nat2 i) = (if i 0 then 0 else i)
unfolding Nat2_def by transfer simp
lemma [code]:
term_of_class.term_of n =
Code_Evaluation.App
(Code_Evaluation.Const (STR ''Test_Import.Nat2'')
(typerep.Typerep (STR ''fun'')
[typerep.Typerep (STR ''Code_Numeral.integer'') [],
typerep.Typerep (STR ''Nat.nat'') []]))
(term_of_class.term_of (integer_of_nat n))
by(simp add: term_of_anything)
If nobody has a better solution, we should think of including this setup in
Code_Target_Nat.
Hope this helps,
Andreas
On 12/08/13 10:53, René Thiemann wrote:
Dear all,
Chris and I have recently ported our libraries IsaFoR and TermFun to the
development version which worked nicely, except for one issue, which arises
when we want to import external proofs into Isabelle.
The below theory compiles in Isabelle 2013 without problems.
The problem is that no matter, how we adjust the imports / code_reflect
settings,
we get different errors with the repository version (6a7ee03902c3) when
invoking the apply eval statement in the last proof:
importing ~~/src/HOL/Library/Code_Target_Numeral, no code_reflect:
works, but not desired
importing ~~/src/HOL/Library/Code_Target_Numeral, code_reflect mentions nat,
but not int (as it worked in 2013):
Error: Type error in function application.
Function: Checker.checker : Checker.inta - Checker.proof - bool
Argument: (Int_of_integer (25 : IntInf.int)) : inta
Reason: Can't unify Checker.inta with inta (Different type constructors)
importing ~~/src/HOL/Library/Code_Target_Numeral, code_reflect mentions both
int and nat:
previous error disappears, but Abstraction violation: constant
Code_Target_Nat.Nat in last apply eval
importing ~~/src/HOL/Library/Code_Target_Numeral, code_reflect mentions only
int, but not nat:
same as before
trying to also load Code_Binary_Nat also did not help.
Any feedback is welcome.
Cheers,
René
theory Test_Import
imports Main
~~/src/HOL/Library/Code_Char
(* in repository: ~~/src/HOL/Library/Code_Target_Numeral *)
(* in 2013: *)
~~/src/HOL/Library/Code_Integer
~~/src/HOL/Library/Code_Natural
begin
definition parse_digit :: char = nat where
parse_digit c = (
if c = CHR ''0'' then 0 else
if c = CHR ''1'' then 1 else
if c = CHR ''2'' then 2 else
if c = CHR ''3'' then 3 else
if c = CHR ''4'' then 4 else
if c = CHR ''5'' then 5 else
if c = CHR ''6'' then 6 else
if c = CHR ''7'' then 7 else
if c = CHR ''8'' then 8 else 9)
datatype proof = N nat | I int
definition parse_proof :: string = proof where
parse_proof input = (case input of
t # d # _ =
if t = CHR ''n'' then N (parse_digit d)
else I (of_nat (parse_digit d)))
definition parse_proof_term :: string = Code_Evaluation.term where
parse_proof_term input == Code_Evaluation.term_of (parse_proof input)
ML {*
structure Parser =
struct
val parse = String.explode # @{code parse_proof_term}
end
*}
fun checker :: int = proof = bool where
checker n (N i) = (of_nat i * of_nat i = n)
| checker n (I i) = (i * i = n)
lemma checker_imp_square: checker n p ⟹ ? x. x * x = n
by (cases p, auto)
(* precompilation of checker-code, so that it does not need to
be recompiled on every invokation of eval later on,
strangely, in 2013 only nat must be registered as datatype, but not int *)
code_reflect Checker
datatypes (* in repo: int = _ and *) nat = _ and proof = _
functions checker Trueprop
declare checker_def[code del]
setup {*
let
fun import_proof_tac ctxt input i =
let
val thy = Proof_Context.theory_of
Re: [isabelle-dev] Problems with Code-Generator
Hi Andreas, Code_Target_Nat implements the type nat as an abstract type (code abstype) with constructor Code_Target_Nat.Nat, i.e., Code_Target_Nat.Nat must not appear in any equation of the code generator. Unfortunately, this declaration also sets up the term_of function for type nat to produce terms with this constructor. In the second example, your import_proof method uses the term_of function to get a term for the given proof (and the number contained in the proof) and introduces along with this number into the goal state. As term_of uses the forbidden constructor Code_Target_Nat.Nat, when you then apply eval, the code generator complains that the abstract constructor is part of the goal state. I now see the problem. The simplest solution is to introduce a new constructor for which you can prove a code equation. For example, the following defines a constructor Nat2 and redefines term_of for naturals to use Nat2. When you add it to your theory before declaring the parser structure, the second example works, too (tested with Isabelle 2b68f4109075). You then also have to reflect both nat and int as datatypes. I integrated this solution also in our larger development, and it works like a charm. Thanks! If nobody has a better solution, we should think of including this setup in Code_Target_Nat. At least from my side, I can confirm that the solution works nicely. Cheers, René ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
