SCP-4387 Re organize isabelle semantic types to become literal programming #134
Conversation
| @@ -367,29 +258,79 @@ and Contract = Close | |||
| | Let ValueId Value Contract | |||
| | Assert Observation Contract | |||
|
|
|||
| type_synonym Accounts = "((AccountId \<times> Token) \<times> Money) list" | |||
| text \<open>@{term Close} is the simplest contract, when we evaluate it, the execution is completed and we | |||
| generate \<^term>\<open>Payment\<close>s \secref{TODO} for the assets in the internal accounts to their default owners | |||
There was a problem hiding this comment.
yes, this depends on wether we move Payment here, or if we split types into DSL and Execution
|
|
||
|
|
||
|
|
||
| \<comment> \<open>TODO: see if we want to add data types of Semantic here (Transaction, etc) or if we want to |
There was a problem hiding this comment.
Perhaps we could collect all of the error and warning types in a new section here?
| record Environment = timeInterval :: TimeInterval | ||
| text \<open>FIXME: Print record: | ||
| @{term [names_short, margin=40]TimeInterval} | ||
| \<close> | ||
|
|
There was a problem hiding this comment.
text \<open>FIXME: Print record: @{term [names_short, margin=40]Transaction}
We could eliminate this problem by moving this section into Core and making it literate there.
Yes, that would be |
SCP-4387 Suggested changes to #134.
There was a problem hiding this comment.
Thank you, it is looking good. I have written a series of pretty pedantic changes. I am not 100% sure all of them are necessary, but I tried to make some things more precise and accurate, add consistency, and fix typos. Also some may not be due to this PR, because some code was moved and I didn't realise, sorry in advance, but still probably good to fix them
isabelle/Core/SemanticsTypes.thy
Outdated
| value using an identifier @{term i}. In this case, the expression @{term v} is | ||
| evaluated, and stored with the name @{term i}. The contract then continues as | ||
| @{term c}. As well as allowing us to use abbreviations, this mechanism also means that we | ||
| can capture and save volatile values that might be changing with time, e.g. the current price of |
There was a problem hiding this comment.
| can capture and save volatile values that might be changing with time, e.g. the current price of | |
| can capture and save volatile values that might be changing with time, e.g.~the current price of |
That is how you prevent the extra space after a stop in LaTeX, I hope it works here too
Given the limitations of Isabelle antiquotes, we decided to modify the organization of the proofs so that they are self documenting and part of the specification.
I attach specification-v3.pdf an exported pdf of the specificationI attach the specification-v3.pdf, modified after @bwbush suggestions.I attach the specification-v3.pdf, modified after @bwbush and @palas suggestions.