Theory Printer_Toy_extended

(******************************************************************************
 * HOL-TOY
 *
 * Copyright (c) 2011-2018 Université Paris-Saclay, Univ. Paris-Sud, France
 *               2013-2017 IRT SystemX, France
 *               2011-2015 Achim D. Brucker, Germany
 *               2016-2018 The University of Sheffield, UK
 *               2016-2017 Nanyang Technological University, Singapore
 *               2017-2018 Virginia Tech, USA
 *
 * All rights reserved.
 *
 * Redistribution and use in source and binary forms, with or without
 * modification, are permitted provided that the following conditions are
 * met:
 *
 *     * Redistributions of source code must retain the above copyright
 *       notice, this list of conditions and the following disclaimer.
 *
 *     * Redistributions in binary form must reproduce the above
 *       copyright notice, this list of conditions and the following
 *       disclaimer in the documentation and/or other materials provided
 *       with the distribution.
 *
 *     * Neither the name of the copyright holders nor the names of its
 *       contributors may be used to endorse or promote products derived
 *       from this software without specific prior written permission.
 *
 * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
 * "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
 * LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR
 * A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT
 * OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,
 * SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT
 * LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE,
 * DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY
 * THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT
 * (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE
 * OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
 ******************************************************************************)

section‹Instantiating the Printer for Toy (II)›

theory  Printer_Toy_extended
imports Meta_Toy_extended
        Printer_Toy
begin

context Print
begin

definition "To_oid = (λOid n ⇒ To_nat n)"

definition ‹of_toy_def_base = (λ ToyDefInteger i ⇒ To_string i
                                | ToyDefReal (i1, i2) ⇒ ‹%s.%s› (To_string i1) (To_string i2)
                                | ToyDefString s ⇒ ‹"%s"› (To_string s))›

fun of_toy_data_shallow where
   "of_toy_data_shallow e = (λ ShallB_term b ⇒ of_toy_def_base b
                             | ShallB_str s ⇒ To_string s
                             | ShallB_self s ⇒ ‹self %d› (To_oid s)
                             | ShallB_list l ⇒ ‹[ %s ]› (String_concat ‹, › (List.map of_toy_data_shallow l))) e"

fun of_toy_list_attr where
   "of_toy_list_attr f e = (λ ToyAttrNoCast x ⇒ f x
                            | ToyAttrCast ty (ToyAttrNoCast x) _ ⇒ ‹(%s :: %s)› (f x) (To_string ty)
                            | ToyAttrCast ty l _ ⇒ ‹%s → toyAsType( %s )› (of_toy_list_attr f l) (To_string ty)) e"

definition ‹of_toy_instance_single toyi =
 (let (s_left, s_right) =
    case Inst_name toyi of
      None ⇒ (case Inst_ty toyi of Some ty ⇒ (‹(›, ‹ :: %s)› (To_string ty)))
    | Some s ⇒
        ( ‹%s%s = ›
            (To_string s)
            (case Inst_ty toyi of None ⇒ ‹› | Some ty ⇒ ‹ :: %s› (To_string ty))
        , ‹›) in
  ‹%s%s%s›
    s_left
    (of_toy_list_attr
      (λl. ‹[ %s ]›
             (String_concat ‹, ›
               (L.map (λ(pre_post, attr, v).
                            ‹%s"%s" = %s› (case pre_post of None ⇒ ‹›
                                                          | Some (s1, s2) ⇒ ‹("%s", "%s") |= › (To_string s1) (To_string s2))
                                          (To_string attr)
                                          (of_toy_data_shallow v))
                         l)))
      (Inst_attr toyi))
    s_right)›

definition "of_toy_instance _ = (λ ToyInstance l ⇒
  ‹Instance %s› (String_concat ‹
     and › (L.map of_toy_instance_single l)))"

definition "of_toy_def_state_core l =
  String_concat ‹, › (L.map (λ ToyDefCoreBinding s ⇒ To_string s
                             | ToyDefCoreAdd toyi ⇒ of_toy_instance_single toyi) l)"

definition "of_toy_def_state _ (floor :: ― ‹polymorphism weakening needed by ⬚‹code_reflect››
                                         String.literal) = (λ ToyDefSt n l ⇒ 
  ‹State%s %s = [ %s ]›
    floor
    (To_string n)
    (of_toy_def_state_core l))"

definition "of_toy_def_pp_core = (λ ToyDefPPCoreBinding s ⇒ To_string s
                                  | ToyDefPPCoreAdd l ⇒ ‹[ %s ]› (of_toy_def_state_core l))"

definition "of_toy_def_pre_post _ (floor :: ― ‹polymorphism weakening needed by ⬚‹code_reflect››
                                            String.literal) = (λ ToyDefPP n s_pre s_post ⇒
  ‹PrePost%s %s%s%s›
    floor
    (case n of None ⇒ ‹› | Some n ⇒ ‹%s = › (To_string n))
    (of_toy_def_pp_core s_pre)
    (case s_post of None ⇒ ‹› | Some s_post ⇒ ‹ %s› (of_toy_def_pp_core s_post)))"

end

lemmas [code] =
  ― ‹def›
  Print.To_oid_def
  Print.of_toy_def_base_def
  Print.of_toy_instance_single_def
  Print.of_toy_instance_def
  Print.of_toy_def_state_core_def
  Print.of_toy_def_state_def
  Print.of_toy_def_pp_core_def
  Print.of_toy_def_pre_post_def

  ― ‹fun›
  Print.of_toy_list_attr.simps
  Print.of_toy_data_shallow.simps

end