Theory Meta_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‹Toy Meta-Model aka. AST definition of Toy (II)›

theory  Meta_Toy_extended
imports "../../../Init"
begin

subsection‹Type Definition›

datatype internal_oid = Oid nat
datatype internal_oids = Oids nat ― ‹start›
                              nat ― ‹oid for assoc (incremented from start)›
                              nat ― ‹oid for inh (incremented from start)›

datatype toy_def_base = ToyDefInteger "string" ― ‹integer digit›
                      | ToyDefReal "string ― ‹integer digit (left)› × string ― ‹integer digit (right)›"
                      | ToyDefString "string"

datatype toy_data_shallow = ShallB_term toy_def_base
                          | ShallB_str string ― ‹binding›
                          | ShallB_self internal_oid
                          | ShallB_list "toy_data_shallow list"

datatype 'a toy_list_attr = ToyAttrNoCast 'a ― ‹inh, own›
                          | ToyAttrCast
                              string ― ‹cast from›
                              "'a toy_list_attr" ― ‹cast entity›
                              'a ― ‹inh, own›

record toy_instance_single = Inst_name :: "string option" ― ‹None: fresh name to be generated›
                             Inst_ty :: "string option" ― ‹type›
                             Inst_attr :: "((  (string ― ‹pre state› × string ― ‹post state›) option
                                               ― ‹state used when ‹toy_data_shallow› is an object variable (for retrieving its oid)›
                                             × string ― ‹name›
                                             × toy_data_shallow) list) ― ‹inh and own›
                                           toy_list_attr"

datatype toy_instance = ToyInstance "toy_instance_single list" ― ‹mutual recursive›

datatype toy_def_base_l = ToyDefBase "toy_def_base list"

datatype 'a toy_def_state_core = ToyDefCoreAdd toy_instance_single
                               | ToyDefCoreBinding 'a

datatype toy_def_state = ToyDefSt  string ― ‹name›
                                  "string ― ‹name› toy_def_state_core list"

datatype toy_def_pp_core = ToyDefPPCoreAdd "string ― ‹name› toy_def_state_core list"
                         | ToyDefPPCoreBinding string ― ‹name›

datatype toy_def_pre_post = ToyDefPP
                              "string option" ― ‹None: fresh name to be generated›
                              toy_def_pp_core ― ‹pre›
                              "toy_def_pp_core option" ― ‹post› ― ‹None: same as pre›

subsection‹Object ID Management›

definition "oidInit = (λ Oid n ⇒ Oids n n n)"

definition "oidSucAssoc = (λ Oids n1 n2 n3 ⇒ Oids n1 (Succ n2) (Succ n3))"
definition "oidSucInh = (λ Oids n1 n2 n3 ⇒ Oids n1 n2 (Succ n3))"
definition "oidGetAssoc = (λ Oids _ n _ ⇒ Oid n)"
definition "oidGetInh = (λ Oids _ _ n ⇒ Oid n)"

definition "oidReinitAll = (λOids n1 _ _ ⇒ Oids n1 n1 n1)"
definition "oidReinitInh = (λOids n1 n2 _ ⇒ Oids n1 n2 n2)"

subsection‹Operations of Fold, Map, ..., on the Meta-Model›

definition "toy_instance_single_empty = ⦇ Inst_name = None, Inst_ty = None, Inst_attr = ToyAttrNoCast [] ⦈"

fun map_data_shallow_self where
   "map_data_shallow_self f e = (λ ShallB_self s ⇒ f s
                                 | ShallB_list l ⇒ ShallB_list (List.map (map_data_shallow_self f) l)
                                 | x ⇒ x) e"

fun map_list_attr where
   "map_list_attr f e = 
     (λ ToyAttrNoCast x ⇒ ToyAttrNoCast (f x)
      | ToyAttrCast c_from l_attr x ⇒ ToyAttrCast c_from (map_list_attr f l_attr) (f x)) e"

definition "map_instance_single f toyi = toyi ⦇ Inst_attr := map_list_attr (L.map f) (Inst_attr toyi) ⦈"

fun fold_list_attr where
   "fold_list_attr cast_from f l_attr accu = (case l_attr of
        ToyAttrNoCast x ⇒ f cast_from x accu
      | ToyAttrCast c_from l_attr x ⇒ fold_list_attr (Some c_from) f l_attr (f cast_from x accu))"

definition "inst_ty0 toyi = (case Inst_ty toyi of Some ty ⇒ Some ty
                                                | None ⇒ (case Inst_attr toyi of ToyAttrCast ty _ _ ⇒ Some ty
                                                                                | _ ⇒ None))"
definition "inst_ty toyi = (case inst_ty0 toyi of Some ty ⇒ ty)"

definition "fold_instance_single f toyi = fold_list_attr (inst_ty0 toyi) (λ Some x ⇒ f x) (Inst_attr toyi)"
definition "fold_instance_single' f toyi = fold_list_attr (Inst_ty toyi) f (Inst_attr toyi)"

end