Fix the record generation in class implementation #5

Merged
adbrucker merged 1 commits from nicolas.meric/Isabelle_DOF:fix-record-generation into master 2021-12-07 18:51:35 +00:00
Collaborator

Hello. Here is a new pull request which fixes a flaw of the record generation in the class implementation.
The commit log:

  • Fix the generation of the record associated with
    a class and used for the logic.
    The old implementation generated a new attribute
    for each attribute defined by a subclass,
    even the ones that were overriding ones of the superclass.
    The new implementation generates the attributes of the subclass
    which are not overriding ones.
    Warning:
    It implies that overridden attributes in a subclass are not
    new attributes added to the theory context.
    So the base name of an attribute will refer to the attribute
    of the last declared class where it is defined.
    If ones wants to refer to atttributes, one should use
    long names, even in the invariants of a subclass definition
    which overrides the attribute used in the invariant.
    For example,
    in ~~/src/ontologies/scholarly_paper/scholarly_paper.thy:

    doc_class technical = text_section +
    definition_list :: "string list" <= "[]"
    status :: status <= "description"
    formal_results :: "thm list"
    invariant L1 :: "λσ::technical. the (level σ) > 0"

    type_synonym tc = technical (* technical content *)

    doc_class example = text_section +
    referentiable :: bool <= True
    status :: status <= "description"
    short_name :: string <= "''''"

    doc_class math_content = tc +
    referentiable :: bool <= True
    short_name :: string <= "''''"
    status :: status <= "semiformal"
    mcc :: "math_content_class" <= "thm"
    invariant s1 :: "λ σ::math_content. ¬referentiable σ ⟶ short_name σ = ''''"
    invariant s2 :: "λ σ::math_content. technical.status σ = semiformal"

    The class math_content overrride the attribute status
    of the class technical, by using the type synonym tc,
    but the base name of this attribute refers
    to the attribute of the class example where it is last defined
    and not just overridden.
    So in the invariant s2 of the class math_content,
    we must use the long name of the attribute,
    i.e. the base name "status" with its qualifier which refers
    to the superclass where it is defined, the class technical.

    Type synonyms as qualifiers are not yet supported.

  • Qualify classes that only override attributes of their superclass
    as vitual classes by adding a virtual attribute.
    This attribute is used to discriminate virtual classes and generate
    an adequate make function to initialize their associated record.
    The implementation uses an hidden attribute (the tag_attribute)
    to force the virtual class to be concrete or the logic
    by having a full new record definition associated with it.
    For example:

    doc_class W =
    a::"int" <= "1"

    doc_class X = W +
    a::"int" <= "2"

    The class X is tagged as a virtual class and
    the record make functions of the classes W and X are:

    W.make W_tag_attribute W_a
    X.make X_tag_attribute X_a X_tag_attribute

    So a record definition is added to the theory context for each class,
    even though a virtual class only overrides
    attributes of its superclass.
    This behavior allows us to support definitions of new default values
    for attributes in the subclass, as shown in the example.

  • Factorize make name components

  • Use Record name components instead of strings to refer to Record
    components

  • Fix typos

Hello. Here is a new pull request which fixes a flaw of the record generation in the class implementation. The commit log: - Fix the generation of the record associated with a class and used for the logic. The old implementation generated a new attribute for each attribute defined by a subclass, even the ones that were overriding ones of the superclass. The new implementation generates the attributes of the subclass which are not overriding ones. Warning: It implies that overridden attributes in a subclass are not new attributes added to the theory context. So the base name of an attribute will refer to the attribute of the last declared class where it is defined. If ones wants to refer to atttributes, one should use long names, even in the invariants of a subclass definition which overrides the attribute used in the invariant. For example, in `~~/src/ontologies/scholarly_paper/scholarly_paper.thy`: doc_class technical = text_section + definition_list :: "string list" <= "[]" status :: status <= "description" formal_results :: "thm list" invariant L1 :: "λσ::technical. the (level σ) > 0" type_synonym tc = technical (* technical content *) doc_class example = text_section + referentiable :: bool <= True status :: status <= "description" short_name :: string <= "''''" doc_class math_content = tc + referentiable :: bool <= True short_name :: string <= "''''" status :: status <= "semiformal" mcc :: "math_content_class" <= "thm" invariant s1 :: "λ σ::math_content. ¬referentiable σ ⟶ short_name σ = ''''" invariant s2 :: "λ σ::math_content. technical.status σ = semiformal" The class math_content overrride the attribute status of the class technical, by using the type synonym tc, but the base name of this attribute refers to the attribute of the class example where it is last defined and not just overridden. So in the invariant s2 of the class math_content, we must use the long name of the attribute, i.e. the base name "status" with its qualifier which refers to the superclass where it is defined, the class technical. Type synonyms as qualifiers are not yet supported. - Qualify classes that only override attributes of their superclass as vitual classes by adding a virtual attribute. This attribute is used to discriminate virtual classes and generate an adequate make function to initialize their associated record. The implementation uses an hidden attribute (the tag_attribute) to force the virtual class to be concrete or the logic by having a full new record definition associated with it. For example: doc_class W = a::"int" <= "1" doc_class X = W + a::"int" <= "2" The class X is tagged as a virtual class and the record make functions of the classes W and X are: W.make W_tag_attribute W_a X.make X_tag_attribute X_a X_tag_attribute So a record definition is added to the theory context for each class, even though a virtual class only overrides attributes of its superclass. This behavior allows us to support definitions of new default values for attributes in the subclass, as shown in the example. - Factorize make name components - Use Record name components instead of strings to refer to Record components - Fix typos
nicolas.meric added 1 commit 2021-12-07 09:18:10 +00:00
d2a6106be5 Fix the record generation in class implementation
- Fix the generation of the record associated with
  a class and used for the logic.
  The old implementation generated a new attribute
  for each attribute defined by a subclass,
  even the ones that were overriding ones of the superclass.
  The new implementation generates the attributes of the subclass
  which are not overriding ones.
  Warning:
  It implies that overridden attributes in a subclass are not
  new attributes added to the theory context.
  So the base name of an attribute will refer to the attribute
  of the last declared class where it is defined.
  If ones wants to refer to atttributes, one should use
  long names, even in the invariants of a subclass definition
  which overrides the attribute used in the invariant.
  For example,
  in ~~/src/ontologies/scholarly_paper/scholarly_paper.thy:

  doc_class technical = text_section +
     definition_list :: "string list" <=  "[]"
     status          :: status <= "description"
     formal_results  :: "thm list"
     invariant L1    :: "λσ::technical. the (level σ) > 0"

  type_synonym tc = technical (* technical content *)

  doc_class example  = text_section +
     referentiable   :: bool <= True
     status          :: status <= "description"
     short_name      :: string <= "''''"

  doc_class math_content = tc +
     referentiable :: bool <= True
     short_name    :: string <= "''''"
     status        :: status <= "semiformal"
     mcc           :: "math_content_class" <= "thm"
     invariant s1  :: "λ σ::math_content. ¬referentiable σ ⟶ short_name σ = ''''"
     invariant s2  :: "λ σ::math_content. technical.status σ = semiformal"

  The class math_content overrride the attribute status
  of the class technical, by using the type synonym tc,
  but the base name of this attribute refers
  to the attribute of the class example where it is last defined
  and not just overridden.
  So in the invariant s2 of the class math_content,
  we must use the long name of the attribute,
  i.e. the base name "status" with its qualifier which refers
  to the superclass where it is defined, the class technical.

  Type synonyms as qualifiers are not yet supported.
- Qualify classes that only override attributes of their superclass
  as vitual classes by adding a virtual attribute.
  This attribute is used to discriminate virtual classes and generate
  an adequate make function to initialize their associated record.
  The implementation uses an hidden attribute (the tag_attribute)
  to force the virtual class to be concrete or the logic
  by having a full new record definition associated with it.
  For example:

  doc_class W =
    a::"int" <= "1"

  doc_class X = W +
    a::"int" <= "2"

  The class X is tagged as a virtual class and
  the record make functions of the classes W and X are:

  W.make W_tag_attribute W_a
  X.make X_tag_attribute X_a X_tag_attribute

  So a record definition is added to the theory context for each class,
  even though a virtual class only overrides
  attributes of its superclass.
  This behavior allows us to support definitions of new default values
  for attributes in the subclass, as shown in the example.
- Factorize make name components
- Use Record name components instead of strings to refer to Record
  components
- Fix typos
nicolas.meric requested review from adbrucker 2021-12-07 09:18:37 +00:00
nicolas.meric requested review from wolff 2021-12-07 09:18:37 +00:00
nicolas.meric requested review from idir.aitsadoune 2021-12-07 09:19:08 +00:00
adbrucker merged commit 84588fccb3 into master 2021-12-07 18:51:35 +00:00
Sign in to join this conversation.
No Label
No Milestone
No Assignees
1 Participants
Notifications
Due Date
The due date is invalid or out of range. Please use the format 'yyyy-mm-dd'.

No due date set.

Dependencies

No dependencies set.

Reference: Isabelle_DOF/Isabelle_DOF#5
No description provided.