Theory Printer_META

(******************************************************************************
 * Citadelle
 *
 * 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 META›

theory  Printer_META
imports Parser_META
        "../../../meta_isabelle/Printer_Isabelle"
        Printer_Toy_extended
begin

context Print
begin

definition "of⇩e⇩n⇩v_section env =
 (if D_output_disable_thy env then
    λ_. ‹›
  else
    of_section env)"

definition "of⇩e⇩n⇩v_semi__theory env =
            (λ Theory_section section_title ⇒ of⇩e⇩n⇩v_section env section_title
             | x ⇒ of_semi__theory env x)"

definition ‹of⇩e⇩n⇩v_semi__theories env =
 (λ Theories_one t ⇒ of⇩e⇩n⇩v_semi__theory env t
  | Theories_locale data l ⇒ 
      ‹locale %s =
%s
begin
%s
end›   (To_string (HolThyLocale_name data))
        (String_concat_map
           ‹
›
           (λ (l_fix, o_assum).
                ‹%s%s› (String_concat_map ‹
› (λ(e, ty). ‹fixes "%s" :: "%s"› (of_semi__term e) (of_semi__typ ty)) l_fix)
                                (case o_assum of None ⇒ ‹›
                                               | Some (name, e) ⇒ ‹
assumes %s: "%s"› (To_string name) (of_semi__term e)))
           (HolThyLocale_header data))
        (String_concat_map ‹

› (String_concat_map ‹

› (of⇩e⇩n⇩v_semi__theory env)) l))›

(* *)

definition "of_floor = (λ Floor1 ⇒ ‹› | Floor2 ⇒ ‹[shallow]› | Floor3 ⇒ ‹[shallow_shallow]›)"

definition "of_all_meta_embedding env =
 (λ META_ctxt floor ctxt ⇒ of_toy_ctxt env (of_floor floor) ctxt
  | META_instance i ⇒ of_toy_instance env i
  | META_def_state floor s ⇒ of_toy_def_state env (of_floor floor) s
  | META_def_pre_post floor p ⇒ of_toy_def_pre_post env (of_floor floor) p)"

definition "of_boot_generation_syntax _ = (λ Boot_generation_syntax mode ⇒
  ‹generation_syntax [ shallow%s ]›
    (let f = ‹ (generation_semantics [ %s ])› in
     case mode of Gen_only_design ⇒ f ‹design›
                | Gen_only_analysis ⇒ f ‹analysis›
                | Gen_default ⇒ ‹›))"

declare[[cartouche_type' = "abr_string"]]

definition "of_boot_setup_env env = (λ Boot_setup_env e ⇒
  of_setup
    env
    (Setup
      (SML.app
        ‹Generation_mode.update_compiler_config›
        [ SML.app
            ‹K›
            [ SML_let_open
                ‹META›
                (― ‹Instead of using›
                 ― ‹‹sml_of_compiler_env_config SML_apply (λx. SML_basic [x]) e››
                 ― ‹the following allows to 'automatically' return an uncurried expression:›
                 SML_basic [sml_of_compiler_env_config sml_apply id e])]])))"

declare[[cartouche_type' = "fun⇩p⇩r⇩i⇩n⇩t⇩f"]]

definition "of_all_meta env = (λ
    META_semi__theories thy ⇒ of⇩e⇩n⇩v_semi__theories env thy
  | META_boot_generation_syntax generation_syntax ⇒ of_boot_generation_syntax env generation_syntax
  | META_boot_setup_env setup_env ⇒ of_boot_setup_env env setup_env
  | META_all_meta_embedding all_meta_embedding ⇒ of_all_meta_embedding env all_meta_embedding)"

definition "of_all_meta_lists env l_thy =
  (let (th_beg, th_end) = case D_output_header_thy env of None ⇒ ([], [])
   | Some (name, fic_import, fic_import_boot) ⇒
       ( [ ‹theory %s imports %s begin›
             (To_string name)
             (of_semi__term (term_binop ⟨STR '' ''⟩
                                        (L.map Term_string
                                               (fic_import @@@@ (if D_output_header_force env
                                                                  | D_output_auto_bootstrap env then
                                                                   [fic_import_boot]
                                                                 else
                                                                   []))))) ]
       , [ ‹›, ‹end› ]) in
  L.flatten
        [ th_beg
        , L.flatten (fst (L.mapM (λl (i, cpt).
            let (l_thy, lg) = L.mapM (λl n. (of_all_meta env l, Succ n)) l 0 in
            (( ‹›
             # ‹%s(* %d ************************************ %d + %d *)›
                 (To_string (if compiler_env_config.more env then ⟨STR ''''⟩ else °integer_escape°)) (To_nat (Succ i)) (To_nat cpt) (To_nat lg)
             # l_thy), Succ i, cpt + lg)) l_thy (D_output_position env)))
        , th_end ])"
end

lemmas [code] =
  ― ‹def›
  Print.of⇩e⇩n⇩v_section_def
  Print.of⇩e⇩n⇩v_semi__theory_def
  Print.of⇩e⇩n⇩v_semi__theories_def
  Print.of_floor_def
  Print.of_all_meta_embedding_def
  Print.of_boot_generation_syntax_def
  Print.of_boot_setup_env_def
  Print.of_all_meta_def
  Print.of_all_meta_lists_def

  ― ‹fun›

end