Comments (3)
Thanks for the interest in Redex!
Unfortunately, the signatures on metafunctions (and similar things in other places) aren't something that redex can reason about statically in a definitive manner. That is, redex currently can only checks that a particular term matches a pattern, not the relationship between two patterns.
I suppose it would be possible, when discovering that flip
is called with a value that doesn't match N
to still check it against all left-hand sides and see if any of those do match, but I think that this would be overly restrictive (e.g., an "else" case might be written with the any
pattern and that would be disallowed but is probably both used and useful).
In the fully general case, the question of what the relationship between two patterns (do they have an empty intersection, is one a subset of the other?) are not things that I know how to compute. If you have ideas on what such an algorithm would look like, I'd be interested! There is already some code (see the overlapping-patterns?
helper function) for a related problem, namely determining if a pattern matches the same expression in two different ways, and a subproblem of that is determining if two patterns have a non-empty intersection (the problem you're asking for here). That code, however is approximate in the sense that it might say "yes there is an intersection" when there isn't really (if it says there isn't an intersection, then there really isn't one (modulo bugs)).
from redex.
That overlapping-patterns?
function sounds perfect for the job. I think it is fine to be an overapproximation here, since people are allowed to be loose with the pattern matching (e.g. any
) and the main intent of this feature would be to catch typos in metafunctions (which are unfortunately very common when working with a big model).
I don't think it changes anything to check one LHS against all the other LHSs, since this is still a pattern-pattern check. My recommendation would be to check the LHSs against the function signature if provided, and otherwise just allow everything. Errors only occur if it is possible to prove that the function signature pattern has empty intersection with the LHS. (You can also do the same checks in RHSs, where clauses and probably many other places.)
The part I struggled with when poking around the code was whether it is possible to run this check at "compilation time" because it seems like define-language
only really runs at run time so I'm not sure if it's possible to get the necessary pattern information. This is probably me just being new to racket and there isn't a problem though.
from redex.
Well, trying to use overlapping-patterns will quickly lead to an understanding of what's insufficient about it.
The way Redex works, you'd extract all the patterns and turn them into the internal format of the patterns at compile time. But then it is probably simplest to do the actually checking when the metafunction definition is evaluated.
And just in the interest of clarity, I'm not sure this is something I'm really ready to take on as I don't see it as the major problem with redex currently, but it is also a non-trivial project.
from redex.
Related Issues (20)
- Defining mutually recursvie judgments/meta-functions HOT 2
- Feature request: tag-with-names for apply-reduction-relation* HOT 2
- test-->>∃ #:steps n passes test if n > than the number of actual reduction steps for a term. HOT 4
- `traces` doesn't draw arrows after "fix layout" HOT 5
- `stepper` doesn't display whole term... unless I *narrow* its box?
- Feature Request: `stepper` with judgment-form use rule names
- Feature request: adjust font for `stepper` HOT 3
- Redex rejects literals at different ellipsis depths in binding form declarations HOT 1
- Generating random expressions sometimes results in an infinite loop
- where/error failures give no information about source of error HOT 6
- where/error failures don't tell you what failed to match
- using judgment-holds within define-relation HOT 1
- Redex's reduction graph windows sneakily hide part of term reductions HOT 1
- where/error doesn't report errors sometimes HOT 8
- Docs missing a word I can't fill in. HOT 1
- `derivation/ps` always causes an error by calling a non-existent method HOT 1
- Default rendering font changed between Racket v8.8 and v8.9? HOT 4
- Redex PDF output contains a wrong font, while Racket REPL renders the correct font HOT 2
- Reduce space between rendered rules of a judgement form HOT 3
Recommend Projects
-
React
A declarative, efficient, and flexible JavaScript library for building user interfaces.
-
Vue.js
🖖 Vue.js is a progressive, incrementally-adoptable JavaScript framework for building UI on the web.
-
Typescript
TypeScript is a superset of JavaScript that compiles to clean JavaScript output.
-
TensorFlow
An Open Source Machine Learning Framework for Everyone
-
Django
The Web framework for perfectionists with deadlines.
-
Laravel
A PHP framework for web artisans
-
D3
Bring data to life with SVG, Canvas and HTML. 📊📈🎉
-
Recommend Topics
-
javascript
JavaScript (JS) is a lightweight interpreted programming language with first-class functions.
-
web
Some thing interesting about web. New door for the world.
-
server
A server is a program made to process requests and deliver data to clients.
-
Machine learning
Machine learning is a way of modeling and interpreting data that allows a piece of software to respond intelligently.
-
Visualization
Some thing interesting about visualization, use data art
-
Game
Some thing interesting about game, make everyone happy.
Recommend Org
-
Facebook
We are working to build community through open source technology. NB: members must have two-factor auth.
-
Microsoft
Open source projects and samples from Microsoft.
-
Google
Google ❤️ Open Source for everyone.
-
Alibaba
Alibaba Open Source for everyone
-
D3
Data-Driven Documents codes.
-
Tencent
China tencent open source team.
from redex.