It should be possible to match against known natural numbers, as demonstrated in regression/match-nat.l10:
w: nat -> world.
w (X+5) <- w X.
The problem also manifests in examples/bulp/cyk-buggy.l10.
In Elton compiling this causes Invariant to be raised, in Smlten it fails silently, which is bad.
$ sml -m sml/smlten.cm
- Read.file "regression/match-nat.l10";
- Deduce.deduce [] (Symbol.symbol "w", [ Term.NatConst' 50 ]);
== Begin deduction ==
Scheduling... 1 stages scheduled.
Running at world w 50 -- 0 rules apply
Iteration 1 -- 0 new fact(s)
== End deduction ==
val it = - : PredSet.set
Making this work will require that the mode checker do something similar to Plus that it does to Equals: check that one of the two numbers can be ground, and probably make sure that one goes as the first argument all the time. Pattern matching against this will amount, in Elton, to a check that the matched constant minus the known constant is greater than zero, and will then bind the smaller number to a new variable.
It should be possible to match against known natural numbers, as demonstrated in
regression/match-nat.l10:The problem also manifests in
examples/bulp/cyk-buggy.l10.In Elton compiling this causes Invariant to be raised, in Smlten it fails silently, which is bad.
Making this work will require that the mode checker do something similar to Plus that it does to Equals: check that one of the two numbers can be ground, and probably make sure that one goes as the first argument all the time. Pattern matching against this will amount, in Elton, to a check that the matched constant minus the known constant is greater than zero, and will then bind the smaller number to a new variable.