Re: [isabelle] Accessing lift_definition from the ML-level

On Fri, 3 Oct 2014, René Thiemann wrote:

playing a little bit further, I could establish part of what I wanted by using lift_def_cmd and converting types and terms back to strings (which are immediately parsed again in lift_def_cmd)

     fun lift_def_ml (binding,mixfix) ty rhs ctxt tactic =
       let val ctxt' = Config.put show_markup false ctxt
           val term_to_string = Print_Mode.setmp [] (Syntax.string_of_term ctxt')
           val typ_to_string = Print_Mode.setmp [] (Syntax.string_of_typ ctxt')
           val state = Lifting_Def.lift_def_cmd
                ((binding, SOME (typ_to_string ty), mixfix), term_to_string rhs, []) ctxt

However, now I am left with turning a Proof.state into a context again (which should be done via the provided tactic). So, is there some common function of type

state -> tactic -> context

In proof.ML I only found functions like

global_qed which take "Method.text_range option * bool", but no tactics.

Just syntactically, this one works out, but I did not try it on concrete

  val term_to_string = YXML.string_of_body o Term_XML.Encode.term;
  val typ_to_string = YXML.string_of_body o Term_XML.Encode.typ;

  fun lift_def_ml (binding, mx) ty rhs tactic lthy =
      val method = (Method.Basic (SIMPLE_METHOD o tactic), Position.no_range);
      |> Lifting_Def.lift_def_cmd
        ((binding, SOME (typ_to_string ty), mx), term_to_string rhs, [])
     |> Proof.global_terminal_proof (method, NONE)

I have made this a bit more canonical according to Isabelle/ML standards, concerning names and argument order. In particular, a lthy: local_theory value should not be called "ctxt". See the "implementation" manual for further important information on Isabelle/ML.

The YXML representation of typ/term values should help to circumvent the accidental omission of proper ML programming interfaces: the inner syntax parser understands that funny machine-oriented notation. Printing terms for parsing them again should never be done in real life.

The Proof.global_terminal_proof is "by method" in Isar syntax.

You've put the term "ML-level of Isabelle" into the subject line. This is leading to bad things as encountered here: people then wrongly think that Isabelle/ML somehow happens in a cold and damp cellar, and "users" are only found in Isar syntax (but I call the second category "end-users").

The comments in $ISABELLE_HOME/src/HOL/Tools/Lifting/lifting.ML use the term "user-friendly" for lift_def_cmd in this defective sense: only a source text interface, without a regular ML entry point (without the "_cmd" suffix). It is quite awkward to imitate surface Isar syntax wrapping in ML.

Isabelle/ML programming is a normal Isabelle user activity, happing at the main user-level of Isabelle. Any package should provide normal ML programming interfaces in parallel to the end-user version -- there are standard patterns to fold the two implementations into one.



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