(****************************************************************************** * 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 (I)› theory Printer_Toy imports Meta_Toy "../../../meta_isabelle/Printer_Pure" begin context Print begin declare[[cartouche_type' = "abr_string"]] definition "concatWith l = (if l = [] then id else sprint2 STR ''(%s. (%s))''´ (To_string (String_concatWith ‹ › (‹λ› # rev l))))" declare[[cartouche_type' = "fun⇩p⇩r⇩i⇩n⇩t⇩f"]] fun of_ctxt2_term_aux where "of_ctxt2_term_aux l e = (λ T_pure pure ⇒ concatWith l (of_pure_term [] pure) | T_to_be_parsed _ s ⇒ concatWith l (To_string s) | T_lambda s c ⇒ of_ctxt2_term_aux (s # l) c) e" definition "of_ctxt2_term = of_ctxt2_term_aux []" definition ‹of_toy_ctxt _ (floor :: ― ‹polymorphism weakening needed by ⬚‹code_reflect›› String.literal) ctxt = (let f_inv = λ T_inv b (ToyProp_ctxt n s) ⇒ ‹ %sInv %s : "%s"› (if b then ‹Existential› else ‹›) (case n of None ⇒ ‹› | Some s ⇒ To_string s) (of_ctxt2_term s) in ‹Context%s %s%s %s› floor (case Ctxt_param ctxt of [] ⇒ ‹› | l ⇒ ‹%s : › (String_concat ‹, › (L.map To_string l))) (To_string (ty_obj_to_string (Ctxt_ty ctxt))) (String_concat ‹ › (L.map (λ Ctxt_pp ctxt ⇒ ‹:: %s (%s) %s %s› (To_string (Ctxt_fun_name ctxt)) (String_concat ‹, › (L.map (λ (s, ty). ‹%s : %s› (To_string s) (To_string (str_of_ty ty))) (Ctxt_fun_ty_arg ctxt))) (case Ctxt_fun_ty_out ctxt of None ⇒ ‹› | Some ty ⇒ ‹: %s› (To_string (str_of_ty ty))) (String_concat ‹ › (L.map (λ T_pp pref (ToyProp_ctxt n s) ⇒ ‹ %s %s: "%s"› (case pref of ToyCtxtPre ⇒ ‹Pre› | ToyCtxtPost ⇒ ‹Post›) (case n of None ⇒ ‹› | Some s ⇒ To_string s) (of_ctxt2_term s) | T_invariant inva ⇒ f_inv inva) (Ctxt_expr ctxt))) | Ctxt_inv inva ⇒ f_inv inva) (Ctxt_clause ctxt))))› end lemmas [code] = ― ‹def› Print.concatWith_def Print.of_ctxt2_term_def Print.of_toy_ctxt_def ― ‹fun› Print.of_ctxt2_term_aux.simps end