/**
 * Holds the rules to evaluate the operators of PHP.
 */
module php/strategy/const-prop/analysis/common/operators

/**
 * The first block of strategies concerns assignment. 
 * Depending on the RHS of the assignment, different things
 * need to be done. 
 * Since assignment is part of the boilerplate-bookkeeping, the
 * strategies are more special.
 */
strategies
  /**
   * Assignment operators
   * http://www.php.net/manual/en/language.operators.assignment.php
   */
  assign-operator-const-prop(main,get,set,valid-get,valid-put,valid-remove|) =  
     ( Assign(Variable(main)     ,main)  
     ; assign-to-variable(get,set,valid-get,valid-put,valid-remove|)
     )
     <+ 
     ( Assign(ArrayAccess(main,main),main)
     ; assign-to-array(main,set,get,valid-put,valid-remove|) 
     )
     <+ 
     ( Assign(StringAccess(main,main),main)
     ; assign-to-array(main,set,get,valid-put,valid-remove|) 
     )
      
  /**
   * Assignment to a variable is special if the RHS is an array. In that case
   * the assignment needs to copy the array. Since it is possible that a second
   * analysis is done, we need to copy the array again with the same new
   * array-id. 
   * If there is no assignment we need to undefine the mapping to the variable,
   * it is not known anymore what the properties are.
   */   
  assign-to-variable(get,set,valid-get,valid-put,valid-remove|) =
     ?Assign(Variable(var), expr)
    ;((
      where(if <has-php-array-value> expr
            then aid     := <get-simple-array-value> expr
               ; newaid  := <copy-php-array> aid 
               ; value   := newaid
               ; try(  
                   <copy-php-array(valid-get,valid-put|newaid)> aid
               )
            else value   := <get-php-simple-value> expr
            end
          ; <add-php-variable-rule> (Variable(var),value)
    )
    ; add-php-simple-value(|value)
    )
    <+ 
    where( 
        <remove-php-variable-rule> Variable(var)
    )) // when done we try the other analysis
    ;try(
      ((where( 
        type := <get> expr
      ; <add-php-variable-rule(valid-put)> (Variable(var),type)
      )
      ; set(|type))
      <+
        where(<remove-php-variable-rule(valid-remove)> Variable(var))
    ))

  /**
   * Assigning to an array is special when the array is the globals-array.
   * Otherwise it is a simple generic assignment.
   */
  assign-to-array(main,set,get,valid-put,valid-remove|) =
   (   ?Assign(ArrayAccess(var,Some(keyExpr)), expr)
   <+  ?Assign(StringAccess(var,keyExpr), expr)
   )
   ; try(
      where( 
       (( aid := <get-simple-array-value> var           
        ; <is-globals-array> aid
        ; name := <get-simple-raw-string-value> keyExpr 
        ; <explode-string; ?[<is-alpha> | _ ]> name
        ; <main> Assign(Variable(Simple(name)),expr)
        )
       <+ 
        <generic-assign-to-array(main,get,valid-put,valid-remove|)> (var,Some(Key(keyExpr)),expr)
       ) 
      ) 
   ; add-php-simple-value(|<get-php-simple-value> expr)
   )
   ; try( set(|<get> expr)
     )
  
  assign-to-array(main,set,get,valid-put,valid-remove|) = 
     ?Assign(ArrayAccess(var,None()), expr) 
   ; where(try( <generic-assign-to-array(main,get,valid-put,valid-remove|)> (var,None(),expr))
      ; add-php-simple-value(|<get-php-simple-value> expr)
   )
   ; try(set(|<get> expr))
   
   /**
    * A reference assign assigns the RHS as a reference to the LHS. Both locations
    * will point to the same value-location.
    */
   assign-operator-const-prop(main,get,set,valid-get,valid-put,valid-remove|) = 
      ReferenceAssign(Variable(id),main)
   ; ?ReferenceAssign(Variable(var1),expr)
   ; where(
      !expr ; 
      ( ?Variable(var2) 
      <+(  (?ArrayAccess(array,Some(keyexpr))       
        <+ (?StringAccess(array,keyexpr))
        )
        ; aid  := <get-simple-array-value> array  
        ; key  := <get-simple-raw-value> keyexpr  
        ; var2 :=  (aid,key)                      
      ))
     ; valueIdentifier := <get-php-value-identifier> var2
     ; <add-php-variable-identifier-rule> (Variable(var1),valueIdentifier)
   )
   ;try(add-php-simple-value(|<get-php-simple-value> Variable(var2)))  
   ;try(set(|<get> Variable(var2)))

   assign-operator-const-prop(main,get,set,valid-get,valid-put,valid-remove|) = //Assignment to array without key
     ?ReferenceAssign(ArrayAccess(<main; ?var>,None()), <main ; ?expr>)
   ; add-php-simple-value(| <generic-reference-assign-to-array(main,get,valid-put,valid-remove|)> (var,None(),expr))

   assign-operator-const-prop(main,get,set,valid-get,valid-put,valid-remove|) = 
     (  ?ReferenceAssign(ArrayAccess(<main; ?var>,Some(<main; ?keyExpr>)), expr)
     <+ ?ReferenceAssign(StringAccess(<main; ?var>,<main; ?keyExpr>), expr)
     )
   ; where(
       aid := <get-simple-array-value> var 
     ; if <not(is-globals-array)> aid
       then value := <generic-reference-assign-to-array(main,get,valid-put,valid-remove|)> (var,Some(Key(keyExpr)),expr)
       else name  := <get-simple-raw-string-value> keyExpr
          ; if <explode-string; ?[is-alpha | _ ]> name
            then value := <main> ReferenceAssign(Variable(Simple(name)),expr)
            else value := <generic-reference-assign-to-array(main,get,valid-put,valid-remove|)> (var,Some(Key(keyExpr)),expr)
            end
       end
   )  
   ; add-php-simple-value(|value)

   /**
    * Generic action for assigning a value to an array. This strategy works
    * on a three-tuple and delivers a value to be returned.
    *
    * @type (arrayvariable, key-expression, expression to assign)
    */
   generic-assign-to-array(main,get,valid-put,valid-remove|) =
       ?(var,key,expr)
     ; aid   := <get-simple-array-value> var
     ; value := <add-array-pairs-to-array(main,get,valid-put,valid-remove|aid)> Pair(key,Value(expr))

   generic-reference-assign-to-array(main,get,valid-put,valid-remove|) =
       ?(var,key,expr)
     ; aid   := <get-simple-array-value> var
     ; value := <add-array-pairs-to-array(main,get,valid-put,valid-remove|aid)> Pair(key,RefValue(expr))

/**
 * The following is const-prop for operators.
 * Since operators manipulate values, we expect every analysis
 * to implement their own handling, just like literals.
 */
strategies
  /**
   * Section for casting 'operators'.
   * @see http://www.php.net/manual/en/language.types.type-juggling.php
   */
  operator-const-prop(main|) =
      IntCast(main)
   ; generic-cast-operator(get-simple-integer-value) 
   
  operator-const-prop(main|) =
      FloatCast(main)
   ; generic-cast-operator(get-simple-float-value) 

  operator-const-prop(main|) =
      BoolCast(main)
   ; generic-cast-operator(get-simple-boolean-value) 
  
  operator-const-prop(main|) =
      StringCast(main)
   ; generic-cast-operator(get-simple-string-value) 
  
  operator-const-prop(main|) =
      ArrayCast(main)
   ; generic-cast-operator(get-simple-array-value) 

  operator-const-prop(main|) =
      NullCast(main)
   ; ?NullCast(expr)
   ; add-php-simple-value(|PHPNull())

   generic-cast-operator(s) =
    ( ?IntCast(expr)
   <+ ?FloatCast(expr)
   <+ ?BoolCast(expr)
   <+ ?StringCast(expr)
   <+ ?ArrayCast(expr) 
    ) 
   ; where( value := <s> expr)
   ; add-php-simple-value(|value)

strategies
  /**
   * Arithmetic Operators
   * see: http://www.php.net/manual/en/language.operators.arithmetic.php
   */
  operator-const-prop(main|) =
     Negative(main) 
  ; ?Negative(expr)
  ; where(
      value  := <get-php-simple-value ; get-php-number-value> expr 
    ; value' := <PHPInteger(<subt> (0,<id>)) <+ PHPFloat(<subt> (0,<id>))>  
  )  
  ; add-php-simple-value(|value')
  
  operator-const-prop(main|) =
     Positive(main) 
  ; ?Positive(expr)
  ; add-php-simple-value(|<get-php-simple-value; get-php-number-value> expr)
   
  operator-const-prop(main|) =
    Plus(main,main) 
  ; generic-aritmetic-operator(add) 

  operator-const-prop(main|) =
    Min(main,main) 
  ; generic-aritmetic-operator(subt) 

  operator-const-prop(main|) =
    Mul(main,main) 
  ; generic-aritmetic-operator(mul) 

  // Mod also results in false with a value of null
  operator-const-prop(main|) =
    Mod(main,main)
  ; ?Mod(x,y)   
  ;  where ( 
       if <get-php-simple-value ; results-in-zero-value> y
       then value := PHPBoolean(False())
       else value := <generic-aritmetic-operator(mod);get-php-simple-value> Mod(x,y)
       end
       )   
  ; add-php-simple-value(|value)
  
  /**
   * Exceptions add div:
   *  - Dividing by zero results in false
   *  - When an int is divided by an int the result is a int,
   *    unless the value is not a fraction. 
   */
  operator-const-prop(main|) =
     Div(main,main) 
  ; ?Div(x,y)
  ;  where ( 
       if <get-php-simple-value ; results-in-zero-value> y
       then value := PHPBoolean(False())
       else tmp1 := <generic-aritmetic-operator(div) ; get-php-simple-value> Div(x,y)
          ; tmp2 := <generic-aritmetic-operator(div, get-php-float-value); get-php-simple-value> Div(x,y)
          ; if <eq> (<get-php-raw-value; real> tmp1, <get-php-raw-value> tmp2) 
            then value := tmp1 //no difference between integer and real division, must be an int
            else value := tmp2
            end
       end
  )
  ; add-php-simple-value(|value)
  
  /**
   * Generic aritmetic operator, evaluates a pair of terms according
   * to a givens strategy. The strategy is applied to the number-values of the given
   * terms. The result is based on the outcome of the strategy. An outcome of type 
   * real is wrapped in a PHPFloat and an integer is wrapped in PHPInteger.
   *
   * @param s          The strategy to combine the two types
   * @param transform  The strategy to be applied after getting the number value.
   *                   default: id
   * @type (term, term) -> PHPInteger OR PHPFloat
   */
  generic-aritmetic-operator(s) =
    generic-aritmetic-operator(s, id)

  generic-aritmetic-operator(s, transform) =
    ( ?Plus(x,y) 
   <+ ?Min(x,y)
   <+ ?Mul(x,y)
   <+ ?Mod(x,y)
   <+ ?Div(x,y)
    )
   ; where( x'   := <get-php-simple-value ; get-php-number-value ; transform ; get-php-raw-value> x
          ; y'   := <get-php-simple-value ; get-php-number-value ; transform ; get-php-raw-value> y
          ; comp := <s> (x',y')
   )       
  ; if <is-real> comp
    then add-php-simple-value(|PHPFloat(comp)) 
    else add-php-simple-value(|PHPInteger(comp))
    end
  
  /**
   * Passes if the given php-simple-value will result in a
   * value of 0.
   *
   * @type PHPSimpleValue -> PHPSimpleValue
   */          
  results-in-zero-value = 
      ?PHPNull() 
   <+ ?PHPBoolean(False())
   <+ ?PHPInteger(0)
   <+ ?PHPFloat(0.0)
   <+ (?PHPString(_) ; get-php-integer-value ; ?PHPInteger(0)) 

strategies
   /**
   * Comparison Operators
   * see: http://www.php.net/manual/en/language.operators.comparison.php
   */
  operator-const-prop(main|) =
     IsEqual(main,main) 
  ; ?IsEqual(x,y)
  ; where(  
     if ((<has-php-string-value> x <+ <has-php-null-value> x); <has-php-string-value> y)
     then value := <generic-equal-operator(get-simple-raw-string-value)> (x, y)
     else if (<has-php-boolean-value> x <+ <has-php-null-value> x)  
          then value := <generic-equal-operator(get-simple-raw-boolean-value)> (x, y)
          else value := <generic-equal-operator(get-simple-raw-integer-value)> (x, y)  
          end 
     end     
  )
  ; add-php-simple-value(|value)
   
  operator-const-prop(main|) = // just reverse result of IsEqual
     IsNotEqual(main,main)
  ; ?IsNotEqual(x,y) 
  ; where( value := <main; get-php-simple-value> Not(IsEqual(x,y)))
  ; add-php-simple-value(|value)

  operator-const-prop(main|) = // If they have the same type then we check IsEqual
     IsIdentical(main,main)
  ; ?IsIdentical(x,y)
  ; where( if <have-same-php-value> (x,y)
           then value := <main; get-php-simple-value> IsEqual(x,y)
           else value := PHPBoolean(False())
           end
  )          
  ; add-php-simple-value(|value)

             
  operator-const-prop(main|) =   // just reverse result of IsIdentical
     IsNotIdentical(main,main)
  ; ?IsNotIdentical(x,y) 
  ; where( value := <main; get-php-simple-value> Not(IsIdentical(x,y)))
  ; add-php-simple-value(|value)                                 
  
  
  operator-const-prop(main|) =
     Greater(main,main)
  ; ?Greater(x,y)
  ; where (
      if (<has-php-string-value> x <+ <has-php-string-value> y)
      then value := <generic-comparison-operator(get-simple-raw-string-value,string-case-gt)> (x, y)
      else value := <generic-comparison-operator(get-simple-raw-integer-value,gt)> (x, y)
      end 
  )
  ; add-php-simple-value(|value)                                 

  operator-const-prop(main|) =   // If equal otherwise if greater
     GreaterEqual(main,main)
  ; ?GreaterEqual(x,y)
  ; where(
      if   <eq> (<main; get-php-simple-value> IsEqual(x,y), PHPBoolean(True()))
      then value := PHPBoolean(True())
      else value := <main; get-php-simple-value> Greater(x,y)
      end
  )
  ; add-php-simple-value(|value)                                 
   
  operator-const-prop(main|) =   // Not GreaterEqual
     Less(main,main)
  ; ?Less(x,y)
  ; add-php-simple-value(|<main; get-php-simple-value> Not(GreaterEqual(x,y)))

  operator-const-prop(main|) =   // Not Greater
     LessEqual(main,main)
  ; ?LessEqual(x,y)
  ; add-php-simple-value(|<main; get-php-simple-value> Not(Greater(x,y)))

//Utils for comparison operators
strategies

 /**
  * Shortcut for generic-comparison-operator(id,equal)
  */
 generic-equal-operator =
   generic-equal-operator(id)

 /**
  * Shortcut for generic-comparison-operator(s,equal)
  */
 generic-equal-operator(s) =
   generic-comparison-operator(s,equal)

 /**
  * Generic comparison operator. Matches a tuple,
  * applies 's' to the terms and compares the terms
  * using the 'comp' strategy. Builds True() if comp succeeds,
  * False() otherwise.
  *
  * @param s    Term   -> Term
  * @param comp (x,y)  -> _
  * @type (term, term) -> PHPBoolean(Boolean)
  */
 generic-comparison-operator(s,comp) =
    ?(x,y)
   ; x' := <s> x
   ; y' := <s> y
   ; if <comp> (x', y')
     then bool := PHPBoolean(True())
     else bool := PHPBoolean(False())
     end

strategies
  /**
   * Logical operators
   * http://www.php.net/manual/en/language.operators.logical.php
   */
  operator-const-prop(main|) = 
    Not(main)
  ; ?Not(expr)
  ; where(
     value := <generic-equal-operator> (<get-simple-boolean-value> expr, PHPBoolean(False()))
 )
 ; add-php-simple-value(|value)                                 

  operator-const-prop(main|) =    
    LAnd(main,main)
  ; generic-logical-op(eq,?True()|True(),False())
    
  operator-const-prop(main|) =    
    And(main,main)
  ; generic-logical-op(eq,?True()|True(),False())
  
  operator-const-prop(main|) =    
    LOr(main,main)
  ; generic-logical-op(eq,?False()|False(),True())
     
  operator-const-prop(main|) =    
    Or(main,main) 
  ; generic-logical-op(eq,?False()|False(),True())
  
  operator-const-prop(main|) =    
    LXor(main,main)
  ; generic-logical-op(eq,id|False(),True())
  
  generic-logical-op(s1,s2|val1,val2) =
   (  ?And(x,y)  <+ ?Or(x,y)
   <+ ?LAnd(x,y) <+ ?LOr(x,y)
   <+ ?LXor(x,y)
   ) 
   ; x' := <get-simple-raw-boolean-value> x
   ; y' := <get-simple-raw-boolean-value> y
   ; if (<s1> (x',y'); <s2> x' )
     then add-php-simple-value(|PHPBoolean(val1))
     else add-php-simple-value(|PHPBoolean(val2))
     end

strategies
  /**
   * String operators
   * http://www.php.net/manual/en/language.operators.string.php
   */
  operator-const-prop(main|) =    
     Concat(main,main)
  ; ?Concat(x,y)
  ; where(
     value := PHPString(<conc-strings> (<get-simple-raw-string-value> x
                                       ,<get-simple-raw-string-value> y
                                       )
                       )
  )  
  ; add-php-simple-value(|value)

strategies   
   /**
    * Increment / Decrement operators
    * http://www.php.net/manual/en/language.operators.increment.php
    */
   operator-const-prop(main|) = 
    (  PostInc(main ; has-php-boolean-value)
    <+ PostDec(main ; has-php-boolean-value)
    <+ PreInc(main  ; has-php-boolean-value) 
    <+ PreDec(main  ; has-php-boolean-value) 
    );
    (  ?PostInc(expr)
    <+ ?PostDec(expr)
    <+ ?PreInc(expr) 
    <+ ?PreDec(expr) 
    )
    ; add-php-simple-value(|<get-php-simple-value> expr)

   /**
    * Section for null
    */
   operator-const-prop(main|) =    //decrement has no effect on null
     ( PostDec(main ; has-php-null-value)
    <+ PreDec(main ; has-php-null-value)
     ) 
     ; add-php-simple-value(|PHPNull())

   operator-const-prop(main|) =    //decrement has effect on null
     ( PostInc(main ; has-php-null-value)
    <+ PreInc(main ; has-php-null-value)
     )
     ; add-php-simple-value(|PHPInteger(1))

   /**
    * Section for integers
    */
   operator-const-prop(main|) =    //result is old value
       PostInc(main ; has-php-integer-value)
    ; ?PostInc(cvar) 
    ; where (cvar' := <get-simple-integer-value> cvar) 
    ; where (<main> Assign(cvar,Plus(cvar,LNumber(Deci("1")))))
    ; add-php-simple-value(|cvar')

   operator-const-prop(main|) =       //result is new value
       PreInc(main ; has-php-integer-value)
    ; ?PreInc(cvar) 
    ; where  (<main; get-php-simple-value; ?cvar'> Assign(cvar,Plus(cvar,LNumber(Deci("1")))))
    ; add-php-simple-value(|cvar')

   operator-const-prop(main|) =    //result is old value
       PostDec(main ; has-php-integer-value)
    ; ?PostDec(cvar) 
    ; where (cvar' := <get-simple-integer-value> cvar) 
    ; where (<main> Assign(cvar,Min(cvar,LNumber(Deci("1")))))
    ; add-php-simple-value(|cvar')

   operator-const-prop(main|) =       //result is new value
       PreDec(main ; has-php-integer-value)
    ; ?PreDec(cvar) 
    ; where  (<main; get-php-simple-value; ?cvar'> Assign(cvar,Min(cvar,LNumber(Deci("1")))))
    ; add-php-simple-value(|cvar')
            
   /**
    * Section for Strings
    */
   operator-const-prop(main|) =        //result is new value
      PreInc(main ; has-php-string-value)
    ; ?PreInc(cvar)
    ; where (value := <get-simple-raw-string-value ; ?str ; php-increment-string-value> cvar)
    ; where (<add-php-variable-rule> (cvar,PHPString(value)))
    ; add-php-simple-value(|PHPString(value))

   operator-const-prop(main|) =        //result is old value
       PostInc(main ; has-php-string-value)
    ; ?PostInc(cvar)
    ; where (value := <get-simple-raw-string-value ; ?str ; php-increment-string-value> cvar)
    ; where (<add-php-variable-rule> (cvar,PHPString(value)))
    ; add-php-simple-value(|PHPString(str))

   operator-const-prop(main|) =        //result is new value
       PreDec(main ; has-php-string-value)
    ; ?PreDec(cvar)
    ; where (value := <get-simple-raw-string-value ; ?str ; php-decrement-string-value> cvar)
    ; where (<add-php-variable-rule> (cvar,PHPString(value)))
    ; add-php-simple-value(|PHPString(value))

   operator-const-prop(main|) =        //result is old value
       PostDec(main ; has-php-string-value)
    ; ?PostDec(cvar)
    ; where (value := <get-simple-raw-string-value ; ?str ; php-decrement-string-value> cvar)
    ; where (<add-php-variable-rule> (cvar,PHPString(value)))
    ; add-php-simple-value(|PHPString(str))

rules
  /**
   * Decrementation of a string. A single-char-string can be decremented.
   * Other strings are ignored.
   */
  php-decrement-string-value:
    str -> str'
      where  [char]:= <explode-string> str
           ; char' := <php-decrement-char> char
           ; str'  := <implode-string> char'

  php-decrement-string-value:
    str -> str
      where <not(explode-string; ?[x])> str

  /**
   * Make sure that we stay in the right range.
   */
  php-decrement-char:
    char -> char'
      where((<lt> (char,123); <gt> (char,97))   // ascii-range for small letters
            <+
            (<lt> (char,91) ; <gt> (char,65)))  // ascii-range for big letters
           ; char' := <subt; ![<id>]> (char,1)

  php-decrement-char:
    122 -> 122

  php-decrement-char:
    90  -> 90

  /** 
   * Incrementing a string. Increment latest charachter and maybe update
   * the one before that if the Z or z is passed.
   */
  php-increment-string-value:
    str -> str'
      where  chars := <explode-string> str
           ; char  := <last> chars
           ; char' := <php-increment-char> char
           ; chars':= <php-combine-incremented-char-lists> (chars,char')
           ; str'  := <implode-string> chars'

  php-increment-char:
    char -> char'
      where((<lt> (char,122); <gt> (char,96))   // ascii-range for small letters
            <+
            (<lt> (char,90) ; <gt> (char,64)))  // ascii-range for big letters
           ; char' := <add; ![<id>]> (char,1)

  php-increment-char:
    122 -> [97,97]     //Adding Z or z goes to AA and aa

  php-increment-char:
    90  -> [65,65]

  /**
   * Combining char-lists that are incremented. Lot of special cases for short
   * lists.
   */
  php-combine-incremented-char-lists:
    ([],chars) -> chars

  php-combine-incremented-char-lists:
    (chars,[]) -> chars

  php-combine-incremented-char-lists:
    (original,[x]) -> chars
      where  <not(?[])> original
           ; chars := <at-last(![x])> original

  php-combine-incremented-char-lists:
    ([x],chars) -> chars

  php-combine-incremented-char-lists:
    (original,[ _ | [y] ]) -> chars
      where   <not(?[])> original
            ; <not(?[x])> original
            ; original'  := <at-last(![])> original //remove last element, add one
            ; original'' := <implode-string; php-increment-string-value; explode-string> original'
            ; chars := <conc> (original'',[y])

// Utils
strategies
 /**
  * Case sensitive equivalent of string-gt
  */
 string-case-gt =
  try((explode-string, explode-string));
  strcmp; ?1

 /**
  * Case sensitive equivalent of string-lt
  */
 string-case-lt =
  try((explode-string, explode-string));
  strcmp; ?-1