[isabelle-dev] Problems with Code-Generator

[René Thiemann]

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