eager-and-lazy-elaboration #17

nicolas.meric · 2022-03-30T06:47:08Z

nicolas.meric commented

2022-03-30 06:47:08 +00:00

No description provided.

nicolas.meric added 4 commits 2022-03-30 06:47:08 +00:00

Loosen dependency on Toplevel.transition ec33e70bbf

Loosen the dependency of the implementation of value* and term*
on Toplevel.transition.
Toplevel.transition should be avoided as it has specific behaviors
like only allowing atomic transactions.

Add eager and lazy elaboration 444d6d077c

- Isabelle uses eager evaluation, so should the elaboration of terms
  which are evaluated.
  The value of instances are now registered in the data tables
  of Isabelle/DOF when fully elaborated, ie,
  term annotation antiquotations proposed by Isabelle/DOF in
  an instance value are replaced by its value before registration
  in Isabelle/DOF data
  A new field, input_term, stores the lazy elaboration
  and is used when elaboration is not wished
  (to print the original input term declared by the user, for example)
- Clean up the simplication mechanism of the internal trace attribute
  (used by monitor classes)

Update DOF manual meta-types as types section 9cd5323063

Types of the implementation language inside the HOL type system
are now represented as datatypes and not just abstract types

Update assert* to use isabelle/DOF evaluation

ci/woodpecker/pr/build Pipeline failed

Details

e4e4a708a5

nicolas.meric merged commit c5a3239d2b into main

2022-03-30 06:48:33 +00:00

nicolas.meric referenced this issue from a commit

2022-03-30 06:48:33 +00:00

Merge pull request 'eager-and-lazy-elaboration' (#17) from nicolas.meric/Isabelle_DOF:eager-and-lazy-elaboration into main

Sign in to join this conversation.

No reviewers

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#17