Fix the record generation in class implementation #5

Merged
adbrucker merged 1 commits from nicolas.meric/Isabelle_DOF:fix-record-generation into master 1 month ago
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 1 month ago
d2a6106be5 Fix the record generation in class implementation
nicolas.meric requested review from adbrucker 1 month ago
nicolas.meric requested review from wolff 1 month ago
nicolas.meric requested review from idir.aitsadoune 1 month ago
adbrucker merged commit 84588fccb3 into master 1 month ago

Reviewers

adbrucker was requested for review 1 month ago
wolff was requested for review 1 month ago
idir.aitsadoune was requested for review 1 month ago
The pull request has been merged as 84588fccb3.
Sign in to join this conversation.
No Label
No Milestone
No Assignees
1 Participants
Notifications
Due Date

No due date set.

Dependencies

This pull request currently doesn't have any dependencies.

Loading…
There is no content yet.