[Liquidity] Extraction to Liquidity is broken for some examples
annenkov opened this issue · 0 comments
annenkov commented
At least the examples CounterRefinementTypes.v
, RustEIP20.v
and CrowdfundingCertifiedExtraction.v
produce Liquidity code that does not compile.
Here is the summary:
CounterRefinementTypes.v
-sig
is identified as a record, since it has one constructor. The problematic part is here: https://github.com/AU-COBRA/ConCert/blob/master/extraction/theories/LPretty.v#L284.is_record_constr
should also check whether projections are defined (projections will be produced either from "real" projections in the case of primitive projections or from names of the arguments)ERC20LiquidityExtraction.v
- move type alias for storage frominit
and move it to the top level; plus, fixing #91 is required. Namesto
andval
are reserved and cannot be used as variable names. The type of thectx
parameter of theinner
local definition in theinit
is wrong. Here is a compilable version after some manual tweaking: https://gist.github.com/annenkov/0c65c701ee958adac16cc8d0a91a2a38CrowdfundingCertifiedExtraction.v
- something is wrong with the remapping ofamount
.
In all the examples above, cosntructors of bool
are printed as True
and False
while they should be true
and false
.