New subject: XRM 78: Add lazy and/or evaluation at the meta-level.

19 Jun 2006

...
 >> "SIGOURE" == SIGOURE Benoit
&lt;sigoure.benoit(a)lrde.epita.fr&gt; writes: 
...
  https://svn.lrde.epita.fr/svn/xrm/trunk
 Index: ChangeLog
 from  SIGOURE Benoit  &lt;sigoure.benoit(a)lrde.epita.fr&gt; 
...
  	Add lazy and/or evaluation at the meta-level.
 	One can now rely on laziness of logical operators to prevent what
 	could be an error at the meta-level, eg: x > 0 & s[x-1]=0 
Brilliant, thanks!


...
     eval-meta-code =
      eval-meta-if
 +    <+ lazy-eval-and
 +    <+ lazy-eval-or
      <+ unroll-meta-for
      <+ unroll-meta-forin
      <+ (expand-pformulas; eval-meta-code) // try again on expansed code.
 @@ -72,6 +81,26 @@
          end
        end    
...
  +  lazy-eval-and =
 +    ?|[ e1 & e2 ]|
 +    ; <prism-desugar> e1
 +    ; try(LitToBool) => e1'
 +    ; if !e1' => False() then
 +        !False()
 +      else
 +        fail
 +      end
 +
 +  lazy-eval-or =
 +    ?|[ e1 | e2 ]|
 +    ; <prism-desugar> e1
 +    ; try(LitToBool) => e1'
 +    ; if !e1' => True() then
 +        !True()
 +      else
 +        fail
 +      end 
I'm surprised not to see some code removed: I believe you are already
handling things such as "true & e" elsewhere.

Re: XRM 78: Add lazy and/or evaluation at the meta-level.