Personnes présentes

• Hai Nguyen Van
• Chantal Keller
• Frédéric Boulanger
• Safouan Taha
• Burkhart Wolff
• Lina Ye

Cartouches in Isabelle

Chantal Keller presents how to use cartouches in Isabelle.

A cartouche consists of arbitrary text, with rendering of its delimiters as like "<...>". In Isabelle, cartouches can be used to delimit embedded content, i.e., as additional syntax for embedded language tokens (types, terms, props). This works better than old-fashioned quotes especially with nested sub-languages. One can also use text cartouches in the outer syntax category <text>.

Cartouches can be used to implement another language, such as domain specific language by providing its own parser in Isabelle. The idea is to apply its own parser for some parts of certains terms while the rest of the terms will be parsed as normally. One can use a parse translation to extract some ML source from a cartouche, which is then evaluated to a term. Hence, the result is considered as the result of the parse translation. For example, one can give a parser that parses text of the form "9*<x+y>", where 9 is an arbitrary natural and x+y is considered as a term. This parser then returns a term that is a list 9 copies of x+y. Thus the term "(<3*<b+c>>, 2)" should be parsed as ([b+c, b+c, b+c], 2).

(Note that the type inference of cartouches is not automatic. With cartouche, one can use Isabelle’s parser to parse for example a sources string as pre-term that may be ill-typed before type-checking it.)

Bu and Chantal have used cartouches in a framework for monadic program testing. In this context, one has to give the abstract state of the program to every variable each time it is used, which can be painful. Cartouches are used to let the user write programs under test as usual in an imperative language, and automatically λ-lift them with the abstract state.

Example

Chantal Keller

theory False
imports String
begin

ML ‹
  local

    (* The transformation function on terms, at the Isabelle level *)
    fun transform_term tm = case tm of
        a $ Const("HOL.False", ty) => a $ Const("HOL.True", ty)
      | _ => tm

  in

    (* A wrapper to use cartouches to transform terms *)
    fun string_tr ctxt (content:(string * Position.T) -> (string * Position.T) list) (args:term list) : term =
      let fun err () = raise TERM ("string_tr", args) in
        (case args of
          [(Const (@{syntax_const "_constrain"}, _)) $ (Free (s, _)) $ p] =>
            (case Term_Position.decode_position p of
              SOME (pos, _) =>
              let val txt = Symbol_Pos.implode(content (s,pos))
                  (* We use Isabelle's parser to parse a (perhaps) ill-typed term *)
                  val tm = Syntax.parse_term ctxt txt
              in
                (* We transform the term and finally type-check it *)
                Syntax.check_term ctxt (transform_term tm)
              end
            | NONE => err ())
        | _ => err ())
      end

  end
›

(* Syntax extension *)
syntax "_cartouche_string" :: "cartouche_position ⇒ string"  ("_")

(* The parse translation gets the cartouche content as a string that is converted into a 
Symbol_Pos.T list using Symbol_Pos.cartouche_content o Symbol_Pos.explode.*)
parse_translation ‹
  [(@{syntax_const "_cartouche_string"},
    K (string_tr @{context} ((Symbol_Pos.cartouche_content : Symbol_Pos.T list -> Symbol_Pos.T list)
                 o (Symbol_Pos.explode : string * Position.T -> Symbol_Pos.T list))))]
›


(* We can now prove this lemma... *)
lemma false :  "‹False›"
by auto

(* ... because we abused the reader! *)
term "False"
term "‹False›"

end