Theory Shadow_DOM_BaseTest

(***********************************************************************************
 * Copyright (c) 2016-2020 The University of Sheffield, UK
 *               2019-2020 University of Exeter, UK
 *
 * 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.
 *
 * 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 HOLDER 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.
 *
 * SPDX-License-Identifier: BSD-2-Clause
 ***********************************************************************************)

section‹Shadow DOM Base Tests›

theory Shadow_DOM_BaseTest
  imports
    "../Shadow_DOM"
begin


definition "assert_throws e p = do {
  h ← get_heap;
  (if (h ⊢ p →⇩e e) then return () else error AssertException)
}"
notation assert_throws ("assert'_throws'(_, _')")

definition "test p h ⟷ h ⊢ ok p"


definition field_access :: "(string ⇒ (_, (_) object_ptr option) dom_prog) ⇒ string ⇒
(_, (_) object_ptr option) dom_prog"  (infix "." 80)
  where
    "field_access m field = m field"

definition assert_equals :: "'a ⇒ 'a ⇒ (_, unit) dom_prog"
  where
    "assert_equals l r = (if l = r then return () else error AssertException)"
definition assert_equals_with_message :: "'a ⇒ 'a ⇒ 'b ⇒ (_, unit) dom_prog"
  where
    "assert_equals_with_message l r _ = (if l = r then return () else error AssertException)"
notation assert_equals ("assert'_equals'(_, _')")
notation assert_equals_with_message ("assert'_equals'(_, _, _')")
notation assert_equals ("assert'_array'_equals'(_, _')")
notation assert_equals_with_message ("assert'_array'_equals'(_, _, _')")

definition assert_not_equals :: "'a ⇒ 'a ⇒ (_, unit) dom_prog"
  where
    "assert_not_equals l r = (if l ≠ r then return () else error AssertException)"
definition assert_not_equals_with_message :: "'a ⇒ 'a ⇒ 'b ⇒ (_, unit) dom_prog"
  where
    "assert_not_equals_with_message l r _ = (if l ≠ r then return () else error AssertException)"
notation assert_not_equals ("assert'_not'_equals'(_, _')")
notation assert_not_equals_with_message ("assert'_not'_equals'(_, _, _')")
notation assert_not_equals ("assert'_array'_not'_equals'(_, _')")
notation assert_not_equals_with_message ("assert'_array'_not'_equals'(_, _, _')")

(* TODO: why don't the code equations of noop work here?  *)
definition removeWhiteSpaceOnlyTextNodes :: "((_) object_ptr option) ⇒ (_, unit) dom_prog"
  where
    "removeWhiteSpaceOnlyTextNodes _ = return ()"

partial_function (dom_prog) assert_equal_subtrees :: "(_::linorder) object_ptr option ⇒
(_::linorder) object_ptr option ⇒ (_, unit) dom_prog"
  where
    [code]: "assert_equal_subtrees ptr ptr' = (case cast (the ptr) of
      None ⇒ (case cast (the ptr) of
        None ⇒ (case cast (the ptr) of
          None ⇒ (case cast (the ptr) of
            None ⇒ error AssertException |
            Some shadow_root_ptr ⇒ (case cast (the ptr') of
              None ⇒ error AssertException |
              Some shadow_root_ptr' ⇒ do {
                mode_val ← get_M shadow_root_ptr mode;
                mode_val' ← get_M shadow_root_ptr' mode;
                (if mode_val = mode_val' then return () else error AssertException);
                child_nodes_val ← get_M shadow_root_ptr RShadowRoot.child_nodes;
                child_nodes_val' ← get_M shadow_root_ptr' RShadowRoot.child_nodes;
                (if length child_nodes_val = length child_nodes_val'
                then return () else error AssertException);
                map_M (λ(ptr, ptr'). assert_equal_subtrees (Some (cast ptr)) (Some (cast ptr')))
                  (zip child_nodes_val child_nodes_val');
                document_ptr ← return (cast shadow_root_ptr);
                document_ptr' ← return (cast shadow_root_ptr');
                document_element_val ← get_M⇩D⇩o⇩c⇩u⇩m⇩e⇩n⇩t document_ptr document_element;
                document_element_val' ← get_M⇩D⇩o⇩c⇩u⇩m⇩e⇩n⇩t document_ptr' document_element;
                (if (document_element_val = None) ∧ (document_element_val' = None)
                then return () else assert_equal_subtrees (Some (cast (the document_element_val)))
                  (Some (cast (the document_element_val'))));
                disconnected_nodes_val ← get_M document_ptr disconnected_nodes;
                disconnected_nodes_val' ← get_M document_ptr' disconnected_nodes;
                (if length disconnected_nodes_val = length disconnected_nodes_val'
                then return () else error AssertException);
                map_M (λ(ptr, ptr'). assert_equal_subtrees (Some (cast ptr)) (Some (cast ptr')))
                  (zip disconnected_nodes_val disconnected_nodes_val');
                doctype_val ← get_M document_ptr doctype;
                doctype_val' ← get_M document_ptr' doctype;
                (if doctype_val = doctype_val' then return () else error AssertException);
                return ()
              })) |
          Some document_ptr ⇒ (case cast (the ptr') of
            None ⇒ error AssertException |
            Some document_ptr' ⇒ do {
              document_element_val ← get_M⇩D⇩o⇩c⇩u⇩m⇩e⇩n⇩t document_ptr document_element;
              document_element_val' ← get_M⇩D⇩o⇩c⇩u⇩m⇩e⇩n⇩t document_ptr' document_element;
              (if (document_element_val = None) ∧ (document_element_val' = None)
              then return () else assert_equal_subtrees (Some (cast (the document_element_val)))
                (Some (cast (the document_element_val'))));
              disconnected_nodes_val ← get_M document_ptr disconnected_nodes;
              disconnected_nodes_val' ← get_M document_ptr' disconnected_nodes;
              (if length disconnected_nodes_val = length disconnected_nodes_val'
              then return () else error AssertException);
              map_M (λ(ptr, ptr'). assert_equal_subtrees (Some (cast ptr)) (Some (cast ptr')))
                (zip disconnected_nodes_val disconnected_nodes_val');
              doctype_val ← get_M document_ptr doctype;
              doctype_val' ← get_M document_ptr' doctype;
              (if doctype_val = doctype_val' then return () else error AssertException);
              return ()
             })) |
        Some character_data_ptr ⇒ (case cast (the ptr') of
          None ⇒ error AssertException |
          Some character_data_ptr' ⇒ do {
            val_val ← get_M character_data_ptr val;
            val_val' ← get_M character_data_ptr' val;
            (if val_val = val_val' then return () else error AssertException)
          })) |
      Some element_ptr ⇒ (case cast (the ptr') of
        None ⇒ error AssertException |
        Some element_ptr' ⇒ do {
          tag_name_val ← get_M element_ptr tag_name;
          tag_name_val' ← get_M element_ptr' tag_name;
          (if tag_name_val = tag_name_val' then return () else error AssertException);
          child_nodes_val ← get_M element_ptr RElement.child_nodes;
          child_nodes_val' ← get_M element_ptr' RElement.child_nodes;
          (if length child_nodes_val = length child_nodes_val' then return () else error AssertException);
          map_M (λ(ptr, ptr'). assert_equal_subtrees (Some (cast ptr)) (Some (cast ptr')))
            (zip child_nodes_val child_nodes_val');
          attrs_val ← get_M element_ptr attrs;
          attrs_val' ← get_M element_ptr' attrs;
          (if attrs_val = attrs_val' then return () else error AssertException);
          shadow_root_opt_val ← get_M element_ptr shadow_root_opt;
          shadow_root_opt_val' ← get_M element_ptr' shadow_root_opt;
          (if (shadow_root_opt_val = None) ∧ (shadow_root_opt_val' = None)
          then return () else assert_equal_subtrees (Some (cast (the shadow_root_opt_val)))
            (Some (cast (the shadow_root_opt_val'))));
          return ()
        }))"
notation assert_equal_subtrees ("assert'_equal'_subtrees'(_, _')")


subsection ‹Making the functions under test compatible with untyped languages such as JavaScript›

fun set_attribute_with_null :: "((_) object_ptr option) ⇒ attr_key ⇒ attr_value ⇒ (_, unit) dom_prog"
  where
    "set_attribute_with_null (Some ptr) k v = (case cast ptr of
      Some element_ptr ⇒ set_attribute element_ptr k (Some v))"
fun set_attribute_with_null2 :: "((_) object_ptr option) ⇒ attr_key ⇒ attr_value option ⇒ (_, unit) dom_prog"
  where
    "set_attribute_with_null2 (Some ptr) k v = (case cast ptr of
      Some element_ptr ⇒ set_attribute element_ptr k v)"
notation set_attribute_with_null ("_ . setAttribute'(_, _')")
notation set_attribute_with_null2 ("_ . setAttribute'(_, _')")

fun get_child_nodes⇩C⇩o⇩r⇩e⇩_⇩D⇩O⇩M_with_null :: "((_) object_ptr option) ⇒ (_, (_) object_ptr option list) dom_prog"
  where
    "get_child_nodes⇩C⇩o⇩r⇩e⇩_⇩D⇩O⇩M_with_null (Some ptr) = do {
      children ← get_child_nodes ptr;
      return (map (Some ∘ cast) children)
    }"
notation get_child_nodes⇩C⇩o⇩r⇩e⇩_⇩D⇩O⇩M_with_null ("_ . childNodes")

fun create_element_with_null :: "((_) object_ptr option) ⇒ string ⇒ (_, ((_) object_ptr option)) dom_prog"
  where
    "create_element_with_null (Some owner_document_obj) tag = (case cast owner_document_obj of
      Some owner_document ⇒ do {
        element_ptr ← create_element owner_document tag;
        return (Some (cast element_ptr))})"
notation create_element_with_null ("_ . createElement'(_')")

fun create_character_data_with_null :: "((_) object_ptr option) ⇒ string ⇒ (_, ((_) object_ptr option)) dom_prog"
  where
    "create_character_data_with_null (Some owner_document_obj) tag = (case cast owner_document_obj of
      Some owner_document ⇒ do {
        character_data_ptr ← create_character_data owner_document tag;
        return (Some (cast character_data_ptr))})"
notation create_character_data_with_null ("_ . createTextNode'(_')")

definition create_document_with_null :: "string ⇒ (_, ((_::linorder) object_ptr option)) dom_prog"
  where
    "create_document_with_null title = do {
      new_document_ptr ← create_document;
      html ← create_element new_document_ptr ''html'';
      append_child (cast new_document_ptr) (cast html);
      heap ← create_element new_document_ptr ''heap'';
      append_child (cast html) (cast heap);
      body ← create_element new_document_ptr ''body'';
      append_child (cast html) (cast body);
      return (Some (cast new_document_ptr))
    }"
abbreviation "create_document_with_null2 _ _ _ ≡ create_document_with_null ''''"
notation create_document_with_null ("createDocument'(_')")
notation create_document_with_null2 ("createDocument'(_, _, _')")

fun get_element_by_id_with_null ::
  "((_::linorder) object_ptr option) ⇒ string ⇒ (_, ((_) object_ptr option)) dom_prog"
  where
    "get_element_by_id_with_null (Some ptr) id' = do {
        element_ptr_opt ← get_element_by_id ptr id';
        (case element_ptr_opt of
          Some element_ptr ⇒ return (Some (cast⇩e⇩l⇩e⇩m⇩e⇩n⇩t⇩_⇩p⇩t⇩r⇩2⇩o⇩b⇩j⇩e⇩c⇩t⇩_⇩p⇩t⇩r element_ptr))
        | None ⇒ return None)}"
  | "get_element_by_id_with_null _ _ = error SegmentationFault"
notation get_element_by_id_with_null ("_ . getElementById'(_')")

fun get_elements_by_class_name_with_null ::
  "((_::linorder) object_ptr option) ⇒ string ⇒ (_, ((_) object_ptr option) list) dom_prog"
  where
    "get_elements_by_class_name_with_null (Some ptr) class_name =
      get_elements_by_class_name ptr class_name ⤜ map_M (return ∘ Some ∘ cast⇩e⇩l⇩e⇩m⇩e⇩n⇩t⇩_⇩p⇩t⇩r⇩2⇩o⇩b⇩j⇩e⇩c⇩t⇩_⇩p⇩t⇩r)"
notation get_elements_by_class_name_with_null ("_ . getElementsByClassName'(_')")

fun get_elements_by_tag_name_with_null ::
  "((_::linorder) object_ptr option) ⇒ string ⇒ (_, ((_) object_ptr option) list) dom_prog"
  where
    "get_elements_by_tag_name_with_null (Some ptr) tag =
      get_elements_by_tag_name ptr tag ⤜ map_M (return ∘ Some ∘ cast⇩e⇩l⇩e⇩m⇩e⇩n⇩t⇩_⇩p⇩t⇩r⇩2⇩o⇩b⇩j⇩e⇩c⇩t⇩_⇩p⇩t⇩r)"
notation get_elements_by_tag_name_with_null ("_ . getElementsByTagName'(_')")

fun insert_before_with_null ::
  "((_::linorder) object_ptr option) ⇒ ((_) object_ptr option) ⇒ ((_) object_ptr option) ⇒
(_, ((_) object_ptr option)) dom_prog"
  where
    "insert_before_with_null (Some ptr) (Some child_obj) ref_child_obj_opt = (case cast child_obj of
      Some child ⇒ do {
        (case ref_child_obj_opt of
          Some ref_child_obj ⇒ insert_before ptr child (cast ref_child_obj)
        | None ⇒ insert_before ptr child None);
        return (Some child_obj)}
    | None ⇒ error HierarchyRequestError)"
notation insert_before_with_null ("_ . insertBefore'(_, _')")

fun append_child_with_null ::
  "((_::linorder) object_ptr option) ⇒ ((_) object_ptr option) ⇒ (_, unit) dom_prog"
  where
    "append_child_with_null (Some ptr) (Some child_obj) = (case cast child_obj of
      Some child ⇒ append_child ptr child
    | None ⇒ error SegmentationFault)"
notation append_child_with_null ("_ . appendChild'(_')")
code_thms append_child_with_null
fun get_body :: "((_::linorder) object_ptr option) ⇒ (_, ((_) object_ptr option)) dom_prog"
  where
    "get_body ptr = do {
       ptrs ← ptr . getElementsByTagName(''body'');
       return (hd ptrs)
    }"
notation get_body ("_ . body")

fun get_document_element_with_null ::
  "((_::linorder) object_ptr option) ⇒ (_, ((_) object_ptr option)) dom_prog"
  where
    "get_document_element_with_null (Some ptr) = (case cast⇩o⇩b⇩j⇩e⇩c⇩t⇩_⇩p⇩t⇩r⇩2⇩d⇩o⇩c⇩u⇩m⇩e⇩n⇩t⇩_⇩p⇩t⇩r ptr of
    Some document_ptr ⇒ do {
      element_ptr_opt ← get_M document_ptr document_element;
      return (case element_ptr_opt of
        Some element_ptr ⇒ Some (cast⇩e⇩l⇩e⇩m⇩e⇩n⇩t⇩_⇩p⇩t⇩r⇩2⇩o⇩b⇩j⇩e⇩c⇩t⇩_⇩p⇩t⇩r element_ptr)
      | None ⇒ None)})"
notation get_document_element_with_null ("_ . documentElement")

fun get_owner_document_with_null :: "((_::linorder) object_ptr option) ⇒ (_, ((_) object_ptr option)) dom_prog"
  where
    "get_owner_document_with_null (Some ptr) = (do {
        document_ptr ← get_owner_document ptr;
        return (Some (cast⇩d⇩o⇩c⇩u⇩m⇩e⇩n⇩t⇩_⇩p⇩t⇩r⇩2⇩o⇩b⇩j⇩e⇩c⇩t⇩_⇩p⇩t⇩r document_ptr))})"
notation get_owner_document_with_null ("_ . ownerDocument")

fun remove_with_null :: "((_::linorder) object_ptr option) ⇒ (_, ((_) object_ptr option)) dom_prog"
  where
    "remove_with_null (Some child) = (case cast child of
      Some child_node ⇒ do {
        remove child_node;
        return (Some child)}
    | None ⇒ error NotFoundError)"
  | "remove_with_null None = error TypeError"
notation remove_with_null ("_ . remove'(')")

fun remove_child_with_null ::
  "((_::linorder) object_ptr option) ⇒ ((_) object_ptr option) ⇒ (_, ((_) object_ptr option)) dom_prog"
  where
    "remove_child_with_null (Some ptr) (Some child) = (case cast child of
      Some child_node ⇒ do {
        remove_child ptr child_node;
        return (Some child)}
    | None ⇒ error NotFoundError)"
  | "remove_child_with_null None _ = error TypeError"
  | "remove_child_with_null _ None = error TypeError"
notation remove_child_with_null ("_ . removeChild")

fun get_tag_name_with_null :: "((_) object_ptr option) ⇒ (_, attr_value) dom_prog"
  where
    "get_tag_name_with_null (Some ptr) = (case cast ptr of
      Some element_ptr ⇒ get_M element_ptr tag_name)"
notation get_tag_name_with_null ("_ . tagName")

abbreviation "remove_attribute_with_null ptr k ≡ set_attribute_with_null2 ptr k None"
notation remove_attribute_with_null ("_ . removeAttribute'(_')")

fun get_attribute_with_null :: "((_) object_ptr option) ⇒ attr_key ⇒ (_, attr_value option) dom_prog"
  where
    "get_attribute_with_null (Some ptr) k = (case cast ptr of
      Some element_ptr ⇒ get_attribute element_ptr k)"
fun get_attribute_with_null2 :: "((_) object_ptr option) ⇒ attr_key ⇒ (_, attr_value) dom_prog"
  where
    "get_attribute_with_null2 (Some ptr) k = (case cast ptr of
      Some element_ptr ⇒ do {
        a ← get_attribute element_ptr k;
        return (the a)})"
notation get_attribute_with_null ("_ . getAttribute'(_')")
notation get_attribute_with_null2 ("_ . getAttribute'(_')")

fun get_parent_with_null :: "((_::linorder) object_ptr option) ⇒ (_, (_) object_ptr option) dom_prog"
  where
    "get_parent_with_null (Some ptr) = (case cast ptr of
      Some node_ptr ⇒ get_parent node_ptr)"
notation get_parent_with_null ("_ . parentNode")

fun first_child_with_null :: "((_) object_ptr option) ⇒ (_, ((_) object_ptr option)) dom_prog"
  where
    "first_child_with_null (Some ptr) = do {
      child_opt ← first_child ptr;
      return (case child_opt of
        Some child ⇒ Some (cast child)
      | None ⇒ None)}"
notation first_child_with_null ("_ . firstChild")

fun adopt_node_with_null ::
  "((_::linorder) object_ptr option) ⇒ ((_) object_ptr option) ⇒ (_, ((_) object_ptr option)) dom_prog"
  where
    "adopt_node_with_null (Some ptr) (Some child) = (case cast ptr of
      Some document_ptr ⇒ (case cast child of
        Some child_node ⇒ do {
          adopt_node document_ptr child_node;
          return (Some child)}))"
notation adopt_node_with_null ("_ . adoptNode'(_')")


fun get_shadow_root_with_null :: "((_) object_ptr option) ⇒ (_, (_) object_ptr option) dom_prog"
  where
    "get_shadow_root_with_null (Some ptr) = (case cast ptr of
      Some element_ptr ⇒ do {
        shadow_root ← get_shadow_root element_ptr;
        (case shadow_root of Some sr ⇒ return (Some (cast sr))
                             | None ⇒ return None)})"
notation get_shadow_root_with_null ("_ . shadowRoot")


subsection ‹Making the functions under test compatible with untyped languages such as JavaScript›
fun get_element_by_id_si_with_null ::
  "(_::linorder) object_ptr option ⇒ string ⇒ (_, (_) object_ptr option) dom_prog"
  where
    "get_element_by_id_si_with_null (Some ptr) id' = do {
        element_ptr_opt ← get_element_by_id_si ptr id';
        (case element_ptr_opt of
          Some element_ptr ⇒ return (Some (cast⇩e⇩l⇩e⇩m⇩e⇩n⇩t⇩_⇩p⇩t⇩r⇩2⇩o⇩b⇩j⇩e⇩c⇩t⇩_⇩p⇩t⇩r element_ptr))
        | None ⇒ return None)}"
  | "get_element_by_id_si_with_null _ _ = error SegmentationFault"

fun find_slot_closed_with_null ::
  "(_::linorder) object_ptr option ⇒ (_, (_) object_ptr option) dom_prog"
  where
    "find_slot_closed_with_null (Some ptr) = (case cast⇩o⇩b⇩j⇩e⇩c⇩t⇩_⇩p⇩t⇩r⇩2⇩n⇩o⇩d⇩e⇩_⇩p⇩t⇩r ptr of
      Some node_ptr ⇒ do {
        element_ptr_opt ← find_slot True node_ptr;
        (case element_ptr_opt of
          Some element_ptr ⇒ return (Some (cast⇩e⇩l⇩e⇩m⇩e⇩n⇩t⇩_⇩p⇩t⇩r⇩2⇩o⇩b⇩j⇩e⇩c⇩t⇩_⇩p⇩t⇩r element_ptr))
        | None ⇒ return None)}
    | None ⇒ error SegmentationFault)"
  | "find_slot_closed_with_null None = error SegmentationFault"
notation find_slot_closed_with_null ("_ . assignedSlot")

fun assigned_nodes_with_null ::
  "(_::linorder) object_ptr option ⇒ (_, (_) object_ptr option list) dom_prog"
  where
    "assigned_nodes_with_null (Some ptr) = (case cast⇩o⇩b⇩j⇩e⇩c⇩t⇩_⇩p⇩t⇩r⇩2⇩e⇩l⇩e⇩m⇩e⇩n⇩t⇩_⇩p⇩t⇩r ptr of
      Some element_ptr ⇒ do {
        l ← assigned_nodes element_ptr;
        return (map Some (map cast⇩n⇩o⇩d⇩e⇩_⇩p⇩t⇩r⇩2⇩o⇩b⇩j⇩e⇩c⇩t⇩_⇩p⇩t⇩r l))}
    | None ⇒ error SegmentationFault)"
  | "assigned_nodes_with_null None = error SegmentationFault"
notation assigned_nodes_with_null ("_ . assignedNodes'(')")

fun assigned_nodes_flatten_with_null ::
  "(_::linorder) object_ptr option ⇒ (_, (_) object_ptr option list) dom_prog"
  where
    "assigned_nodes_flatten_with_null (Some ptr) = (case cast⇩o⇩b⇩j⇩e⇩c⇩t⇩_⇩p⇩t⇩r⇩2⇩e⇩l⇩e⇩m⇩e⇩n⇩t⇩_⇩p⇩t⇩r ptr of
      Some element_ptr ⇒ do {
        l ← assigned_nodes_flatten element_ptr;
        return (map Some (map cast⇩n⇩o⇩d⇩e⇩_⇩p⇩t⇩r⇩2⇩o⇩b⇩j⇩e⇩c⇩t⇩_⇩p⇩t⇩r l))}
    | None ⇒ error SegmentationFault)"
  | "assigned_nodes_flatten_with_null None = error SegmentationFault"
notation assigned_nodes_flatten_with_null ("_ . assignedNodes'(True')")

fun get_assigned_elements_with_null ::
  "(_::linorder) object_ptr option ⇒ (_, (_) object_ptr option list) dom_prog"
  where
    "get_assigned_elements_with_null (Some ptr) = (case cast⇩o⇩b⇩j⇩e⇩c⇩t⇩_⇩p⇩t⇩r⇩2⇩e⇩l⇩e⇩m⇩e⇩n⇩t⇩_⇩p⇩t⇩r ptr of
      Some element_ptr ⇒ do {
        l ← assigned_nodes element_ptr;
        l ← map_filter_M (return ∘ cast⇩n⇩o⇩d⇩e⇩_⇩p⇩t⇩r⇩2⇩e⇩l⇩e⇩m⇩e⇩n⇩t⇩_⇩p⇩t⇩r) l;
        return (map Some (map cast l))}
    | None ⇒ error SegmentationFault)"
  | "get_assigned_elements_with_null None = error SegmentationFault"
notation get_assigned_elements_with_null ("_ . assignedElements'(')")

fun get_assigned_elements_flatten_with_null ::
  "(_::linorder) object_ptr option ⇒ (_, (_) object_ptr option list) dom_prog"
  where
    "get_assigned_elements_flatten_with_null (Some ptr) = (case cast⇩o⇩b⇩j⇩e⇩c⇩t⇩_⇩p⇩t⇩r⇩2⇩e⇩l⇩e⇩m⇩e⇩n⇩t⇩_⇩p⇩t⇩r ptr of
      Some element_ptr ⇒ do {
        l ← assigned_nodes_flatten element_ptr;
        return (map Some (map cast⇩n⇩o⇩d⇩e⇩_⇩p⇩t⇩r⇩2⇩o⇩b⇩j⇩e⇩c⇩t⇩_⇩p⇩t⇩r l))}
    | None ⇒ error SegmentationFault)"
  | "get_assigned_elements_flatten_with_null None = error SegmentationFault"
notation get_assigned_elements_flatten_with_null ("_ . assignedElements'(True')")

fun createTestTree ::
  "(_::linorder) object_ptr option ⇒ (_, string ⇒ (_, (_) object_ptr option) dom_prog) dom_prog"
  where
    "createTestTree (Some ref) = do {
      tups ← to_tree_order_si ref ⤜ map_filter_M (λptr. do {
        (case cast ptr of
          Some element_ptr ⇒ do {
            iden_opt ← get_attribute element_ptr ''id'';
            (case iden_opt of
              Some iden ⇒ return (Some (iden, ptr))
            | None ⇒ return None)
          }
        | None ⇒ return None)});
      return (return ∘ map_of tups)
    }"
  | "createTestTree None = error SegmentationFault"


end