referential-equivalence-first-draft #4

Merged
adbrucker merged 2 commits from nicolas.meric/Isabelle_DOF:referential-equivalence-first-draft into master 1 week ago
Collaborator

Implement built-ins referential equivalence

  • Add a first implementation of a referential equivalence
    for the built-ins term annotations (TA)
  • Some built-ins remain as unspecified constants:
    • the docitem TA offers a way to check the reference of
      class instances without checking the instances type.
      It must be avoided for certification
    • the termrepr TA is left as an unspecified constant for now.
      A major refactoring of code should be done to enable
      referential equivalence for termrepr, by changing the dependency
      between the Isa_DOF theory and the Assert theory.
      The assert_cmd function in Assert should use the value* command
      functions, which make the elaboration of the term
      referenced by the TA before passing it to the evaluator
  • Update the Evaluation test theory to test the referential equivalence
    and expose some of current implementation limitations
  • Add a warning about the docitem TA in the TermAntiquotations theory
Implement built-ins referential equivalence - Add a first implementation of a referential equivalence for the built-ins term annotations (TA) - Some built-ins remain as unspecified constants: - the docitem TA offers a way to check the reference of class instances without checking the instances type. It must be avoided for certification - the termrepr TA is left as an unspecified constant for now. A major refactoring of code should be done to enable referential equivalence for termrepr, by changing the dependency between the Isa_DOF theory and the Assert theory. The assert_cmd function in Assert should use the value* command functions, which make the elaboration of the term referenced by the TA before passing it to the evaluator - Update the Evaluation test theory to test the referential equivalence and expose some of current implementation limitations - Add a warning about the docitem TA in the TermAntiquotations theory
nicolas.meric added 3 commits 3 weeks ago
664aede4c0 First draft of the value* command implementation
6ac1445147 Change the implementation of the tag attribute
08c101c544 Implement built-ins referential equivalence
nicolas.meric requested review from wolff 3 weeks ago
nicolas.meric requested review from adbrucker 3 weeks ago
adbrucker merged commit 1d497db5cf into master 1 week ago

Reviewers

wolff was requested for review 3 weeks ago
adbrucker was requested for review 3 weeks ago
The pull request has been merged as 1d497db5cf.
Sign in to join this conversation.
No reviewers
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.