search

radeusgd / QuotedPatternMatchingProof

A mechanized proof of soundness of calculus defined in A Theory of Quoted Code Patterns which is a formalization of pattern matching on code available in Scala 3 as part of its new macro system.
3 stars 0 forks source link

Add pattern matching #12

Open radeusgd opened 4 years ago

radeusgd commented 4 years ago

Some experiments on how to handle patterns on syntactic level done in 97d6275ee35547886792f4cca89b1cab4c96f25b Proofs of properties will be handled after the simpler calculus (quotes and splices) is proven.

radeusgd commented 4 years ago

We decided to go for non-nested pattern matching, a calculus with this kind of pattern matching is proven to have the Progress and Preservation properties in 3ec9d044c71ba6f1eef021d0f24f8d3343e6c4ac.