Re: [isabelle] Proof of concept: BNF-based records



On Fr, 2018-02-16 at 20:52 +0100, Makarius wrote:
> On 16/02/18 19:48, Peter Lammich wrote:
> > 
> > So I don't feel so bad anymore about writing syntax translations
> > tgat
> > depend on a configuration flag from the local context ... I did
> > this
> > trick recently to enable advanced syntax in a bundle ... the
> > problem was
> > that some translations that match on the outermost constant of an
> > expression are not supposed to return identity ... this required
> > further
> > workarounds and makes it all feel like a bad hack.
> Can you point to the sources?

No, but I can include a stripped-down example. Basically, the print and
parse translations will raise Match if they are disabled by a
configuration option.

See the last lines of attached text to see an example how it is
supposed to work.


The decomposition of strings looks ughly, I basically copied it from
String_Syntax.ML

--
  Peter


theory Scratch
imports Main
begin

typedecl aexp
consts V0 :: "string ⇒ aexp"

ML ‹
  structure IMP_Translation = struct
  
    val cfg_var_syntax = Attrib.setup_config_bool @{binding
IMP_var_syntax} (K false)
  
    fun 
      var_tr ctxt [(c as Const (@{syntax_const "_constrain"}, _)) $ t $
u] =
        c $ var_tr ctxt [t] $ u
    | var_tr _ [Free (str,_)] = Syntax.const (@{const_syntax V0}) $
HOLogic.mk_string str
    | var_tr _ ts = raise (TERM ("V0",ts))
    
    fun 
      dest_list_syntax (Const (@{const_syntax List.Cons},_)$x$xs) 
        = x::dest_list_syntax xs
    | dest_list_syntax (Const (@{const_syntax List.Nil},_)) = []
    | dest_list_syntax _ = raise Match
    
    fun 
      dest_char_syntax (Const (@{const_syntax String.Char}, _) $ c) = 
        let
          val n = Numeral.dest_num_syntax c
          val s = chr n
        in
          s
        end
    | dest_char_syntax _ = raise Match    
    
    fun dest_var_syntax t = let
      val s =
          dest_list_syntax t 
        |> map dest_char_syntax 
        |> implode
      val _ = Symbol.is_ascii_identifier s orelse raise Match  
    in
      s
    end
    
    fun 
      var_tr' _ [t:term] = 
        Syntax.const @{const_syntax "V0"} $ Syntax.const
(dest_var_syntax t)
    | var_tr' _ _ = raise Match

    fun if_var_syntax f ctxt = 
      if Config.get ctxt cfg_var_syntax then
        f ctxt
      else
        raise Match
    
    
    val _ = Theory.setup (
      Sign.print_translation [
        (@{const_syntax "V0"}, if_var_syntax var_tr')
      ]
    )
    val _ = Theory.setup (
      Sign.parse_translation [
        (@{const_syntax "V0"}, if_var_syntax var_tr)
      ]
    )

    
  end
›


bundle IMP_Syntax begin

notation V0 ("$_" [100] 100)

declare [[IMP_var_syntax]]

end

term "V0 ''x''"  (* Printed as V0 ''x'' *)
term "$x"       (* Error *)

context
  includes IMP_Syntax
begin
  term "V0 ''x''" (* Printed as $x *)
  term "$x"       (* Printed as $x*)
end





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