/**
 * Holds the decleration of the constructors and several useful
 * strategies for PHP-types. This includes the getting of a simple value,
 * the getting of a value of a specific type and the retrieving of a raw value.
 * It also includes strategies for storing and retrieving array's.
 *
 * @author Eric Bouwers
 */
module php/strategy/const-prop/types
imports
  php/reflect/oo/classes       //An array is represented as a class

signature
  constructors
    PHPSimpleValue : PHPPrimitiveType -> PHPSimpleValue

    PHPBoolean : True             -> PHPPrimitiveType
    PHPBoolean : False            -> PHPPrimitiveType

    PHPInteger : Int              -> PHPPrimitiveType

    PHPFloat   : Real             -> PHPPrimitiveType

    PHPString  : String           -> PHPPrimitiveType

    PHPNull    :                     PHPPrimitiveType

    PHPArray   : String           -> PHPPrimitiveType

    PHPObject  : String * String  -> PHPPrimitiveType
    
// Annotation rules
rules
  /**
   * Extracts the PHPSimple-value of the annotations of a term.
   * It first evaluates the given term using main-analysis-const-prop 
   *
   * @type Term -> PHPPrimitiveType
   */
  get-php-simple-value:
    t{a*} -> val
      where    <fetch-elem(?PHPSimpleValue(val))> a*           //no luck?

  /**
   * Adds a PHPSimpleValue annotation. Removes all PHPSimpleValues
   * that the term might have.
   *
   * @param val PHPPrimitiveType to add
   * @type Term -> Term
   */
  add-php-simple-value(|val):
    t{a*} -> t{annos*}
      where  b*     := <remove-all(?PHPSimpleValue(_))> a*
           ; annos* := [PHPSimpleValue(val) | b*]
 
  /**
   * Removes an PHPSimpleValue annotation from a term.
   *
   * @type Term -> Term
   */
  remove-php-simple-value:
    t{a*} -> t{b*}
      where b* := <remove-all(?PHPSimpleValue(_))> a*

  /**
   * Checks wheter or not a term has a php simple value
   *
   * @type Term -> Term
   */
  has-php-simple-value:
    t{a*} -> t{a*}
      where <fetch-elem(?PHPSimpleValue(val))> a*

// Raw value rules
rules
  /**
   * Extracts the raw value of a PHPPrimitive.
   *
   * @type PHPPrimitive -> primitive value
   */
  get-php-raw-value:
     PHPBoolean(b) -> b

  get-php-raw-value:
     PHPInteger(i) -> i

  get-php-raw-value:
     PHPFloat(f) -> f

  get-php-raw-value:
     PHPString(s) -> s

  get-php-raw-value:
     PHPNull() -> PHPNull()

// check value type
strategies
  /**
   * Answers the question: Does this term has a value of this type?
   * Succeeds if it does.
   */
  has-php-string-value =
    where ( get-php-simple-value
            ; ?PHPString(_)
          )

  has-php-integer-value =
    where ( get-php-simple-value
           ; ?PHPInteger(_)
          )

  has-php-float-value =
    where ( get-php-simple-value
           ; ?PHPFloat(_)
          )

  has-php-boolean-value =
    where ( get-php-simple-value
           ; ?PHPBoolean(_)
          )

  has-php-null-value =
    where ( get-php-simple-value
           ; ?PHPNull()
          )

  has-php-array-value =
    where ( get-php-simple-value
           ; ?PHPArray(_)
          )


// equality
strategies
  /**
   * Checks wheter both values of a tuple have the same value type.
   * Succeeds if they have the same value type.
   *
   * @type (term, term) -> (term,term)
   */
  have-same-php-value =
     ?(<has-php-string-value> , <has-php-string-value>)
  <+ ?(<has-php-integer-value>, <has-php-integer-value>)
  <+ ?(<has-php-float-value>  , <has-php-float-value>)
  <+ ?(<has-php-boolean-value>, <has-php-boolean-value>)
  <+ ?(<has-php-null-value>   , <has-php-null-value>)
  <+ ?(<has-php-array-value>  , <has-php-array-value>)

// Short cut rules. Extracting the raw value of a certain term
rules
  /**
   * Extracts the simple raw string value of a term.
   *
   * @type Term -> String
   */
  get-simple-raw-string-value:
    t -> value
      where value := <get-simple-raw-value(get-php-string-value)> t

  get-simple-raw-boolean-value:
    t -> value
      where value := <get-simple-raw-value(get-php-boolean-value)> t

  get-simple-raw-integer-value:
    t -> value
      where value := <get-simple-raw-value(get-php-integer-value)> t

  get-simple-raw-float-value:
    t -> value
      where value := <get-simple-raw-value(get-php-float-value)> t

  get-simple-raw-array-value:
    t -> value
      where value := <get-simple-raw-value(get-php-array-value)> t

  get-simple-raw-value:
    t -> value
      where value := <get-simple-raw-value(id)> t

// Short cut rules. Extracting the raw value of a certain term
rules
  /**
   * Extracts the simple string value of a term.
   *
   * @type Term -> PHPString
   */
  get-simple-string-value:
    t -> value
      where value := <get-simple-value(get-php-string-value)> t

  /**
   * @type Term -> PHPBoolean
   */
  get-simple-boolean-value:
    t -> value
      where value := <get-simple-value(get-php-boolean-value)> t

  /**
   * @type Term -> PHPInteger
   */
  get-simple-integer-value:
    t -> value
      where value := <get-simple-value(get-php-integer-value)> t

  /**
   * @type Term -> PHPFloat
   */
  get-simple-float-value:
    t -> value
      where value := <get-simple-value(get-php-float-value)> t

  /**
   * @type Term -> PHPArray
   */
  get-simple-array-value:
    t -> value
      where ( Variable(Simple(name)) := t
            ; value := <PHPSuperGlobalValue> name
            )
         <+ value := <get-simple-value(get-php-array-value)> t

strategies
  /**
   * Get the simple value of a term. Extracts the value and 
   * rewrites to raw value. The given strategy is applied before
   * extracting the raw value.
   *
   * @type Term -> Real or Boolean or String or Null or Integer
   */
  get-simple-raw-value(s) =
    get-php-simple-value
  ; s
  ; get-php-raw-value
  
  /**
   * Get the simple value of a term.
   *
   * @type Term -> Real or Boolean or String or Null or Integer
   */
  get-simple-value(s) =
    get-php-simple-value
  ; s
  
strategies
/** 
 * Representation of an array. An Array is represented as a set
 * of dynamic rules, each rule looks like:
 *  EvalPHPArray: (ArrayId, Key) -> Value
 *
 */
  /**
   * Adds an entry to the AID with a key and a value.
   *
   * @param key   The key to use, must be an Integer or String
   * @param value The value to add
   * @type PHPArrayId -> PHPArrayId
   */
  add-array-entry(|key,value) =
    add-array-entry(php-val-id-add-rule|key,value)

  add-array-entry(valid-put|key,value) = ?array ;
       highest := <get-next-array-indice> array
     ; if   <is-int> key ; <gt> (key,highest)
       then <set-next-array-indice(|<add> (key,1))> array
       end
     ; if   <is-int <+ is-string> key
       then   value-identifier := <get-php-value-identifier> (array,key) 
            ; rules(EvalPHPArray: (array,key)      -> value-identifier)
            ; valid-put(|value-identifier,value)
            ; rules(EvalPHPIsRefEntry: (array,key) -> False())
       else fail
       end
     ; !array

  add-array-entry-reference(|key,value-identifier) = ?array ;
       highest := <get-next-array-indice> array
     ; if   <is-int> key ; <gt> (key,highest)
       then <set-next-array-indice(|<add> (key,1))> array
       end
     ; if   <is-int <+ is-string> key 
       then  rules(EvalPHPArray: (array,key) -> value-identifier)
           ; rules(EvalPHPIsRefEntry: (array,key) -> True())
           ; !(array,key)
           ; !value-identifier
       else fail
       end
     ; !array


  /**
   * Adds an entry to the ArrayId with only  a value.
   *
   * @param value The value to add
   * @type PHPArrayId -> PHPArrayId
   */
  add-array-entry(|value) =  
     add-array-entry(php-val-id-add-rule|value)

  add-array-entry(valid-put|value) = ?array ;
       key := <get-next-array-indice> array
     ; <set-next-array-indice(|<add> (key,1))> array
     ; <add-array-entry(valid-put|key,value)>  array
     ; !key
      
  add-array-entry-reference(|value-identifier) = ?array ;
       key := <get-next-array-indice> array
     ; <set-next-array-indice(|<add> (key,1))> array
     ; <add-array-entry-reference(|key,value-identifier)>  array
     ; !array

  /**
   * Retrieve an entry from the array.
   *
   * @param key   The key of the value
   * @type PHPArrayId -> Value
   */
  get-array-entry(|key) =
    get-array-entry(php-val-id-get-rule|key)

  get-array-entry(valid-get|key) = ?array;
      <EvalPHPArray> (array,key) 
    ; valid-get 

  /**
   * Removes an entry from the array.
   *
   * @param key   The key of the value
   * @type PHPArrayId -> PHPArrayId
   */
  remove-array-entry(|key) =
    remove-array-entry(php-val-id-remove-rule|key)
  
  remove-array-entry(valid-remove|key) = ?array;
      value-identifier := <get-php-value-identifier> (array,key)
    ; valid-remove(|value-identifier)
//    ; rules(EvalPHPArray :- (array,key))
    ; try(rules(EvalPHPIsRefEntry :- (array,key)))
    ; !array

  /** 
   * Removes all entries from an array. This does not
   * include the resetting of the next-indice.
   *
   * @type ArrayId -> ArrayId
   */
  remove-all-array-entries =
    remove-all-array-entries(php-val-id-remove-rule)

  remove-all-array-entries(valid-remove) = ?array;
     keys := <get-array-keys> array
   ; <map (\ key -> <remove-array-entry(valid-remove|key) > array \)> keys
   ; !array
   
  /**
   * Sets the next array indice that should be given to a new entry
   * without a key.
   *
   * @param current The current highest index
   * @type PHPArrayId -> PHPArrayId
   */
  set-next-array-indice(|next) = ?array ;
      rules(EvalPHPNextIndex: array -> next )
    ; !array

  /**
   * Increases the highest index value of this array with the given amount.
   *
   * @param amount The delta to add to the current highest index
   * @type PHPArrayId -> PHPArrayId
   */
  increase-highest-array-index(|amount) = ?array ;
       current := <get-next-array-indice> array
     ; <set-next-array-indice(|<add> (current,amount))> array

  /**
   * Get the array indice that should be given to a new entry
   * without a key.
   *
   * @type PHPArrayId -> Integer
   */
  get-next-array-indice = ?array ;
   (( <EvalPHPNextIndex> array      //intentionally
    )
    <+
    ( ?PHPArray(<string-starts-with(|"superglobal")>)  // first call to a superglobal
    ; <set-next-array-indice(|0)> array
    ; <get-next-array-indice> array
    ))

  /**
   * Returns a list with all values of the array.
   *
   * @type PHPArrayId -> List(a)
   */
  get-array-values = 
    get-array-values(php-val-id-get-rule)

  get-array-values(valid-get) = ?array;
     keys := <get-array-keys> array
   ; <map (\ key -> <get-array-entry(valid-get|key) > array \)> keys

  /**
   * Returns a list with all keys of the array.
   *
   * @type PHPArrayId -> List(a)
   */
  get-array-keys = 
    get-array-keys(php-val-id-get-rule)

  get-array-keys(valid-get) = ?array ;
     allKeys  := <dr-all-keys(|"EvalPHPArray")> 
     // Get the keys that match the array, but also check of the rule still holds.
     // undefine does NOT remove the rule from the ruleset, the value becomes []
     // TODO: ask how to actually remove a dynamic rule...
   ; ruleKeys := <retain-all({ key : ?(array,key); <get-array-entry(valid-get|key) > array ; !key })> allKeys


 /**
   * Returns a cope of the array. This makes a new set of dynamic rules
   * with the a new id.
   *
   * @type PHPArrayId -> PHPArrayId
   */
  copy-php-array =
    copy-php-array(php-val-id-get-rule,php-val-id-add-rule)
     
  copy-php-array(valid-get,valid-put) = 
     where( newarray := <get-new-php-array-id>)
   ; copy-php-array(valid-get,valid-put|newarray)
  
  copy-php-array(valid-get,valid-put|newarray) = ?array;
    keys     := <get-array-keys(valid-get)> array 
  ; <map(copy-php-array-value(valid-get,valid-put|array,newarray))> keys                 // values
  ; <set-next-array-indice(|<get-next-array-indice> array)> newarray  // next index
  ; !newarray

  /**
   * Copies one entry from an array to an other. Must be
   * applied to a key.
   *
   * @type key -> PHPArrayId
   */
  copy-php-array-value(valid-get,valid-put|from,to) =
    ?key
   ; if True() := <EvalPHPIsRefEntry> (from,key)                    // references should be copied
     then value-identifier := <get-php-value-identifier> (from,key)
        ; <add-array-entry-reference(|key,value-identifier)> to
        ; !to
     else value := <get-array-entry(valid-get|key)> from
        ; <add-array-entry(valid-put|key,value)> to
        ; !to
     end

strategies
   /**
    * Generates an unique PHPArray(name) id that can be
    * used to keep track of an array.
    *
    * @type _ -> PHPArray(uniquename)
    */
  get-new-php-array-id =
      <newname> "php_array_"
    ; !PHPArray(<id>)
    ; set-next-array-indice(|0) //next will update the integer itself
    
  /**
   * Removes all dynamic rules that are involved in constant propagation.
   * Happens when an include cannot be performed.
   * @type _ -> _
   */
  php-remove-all-eval-dynamic-rules =
   php-remove-all-eval-dynamic-rules(|"EvalPHPValId")

  php-remove-all-eval-dynamic-rules(|valid-name) =
    remove-rules-from-ruleset(|"EvalPHPVar")
   ;remove-rules-from-ruleset(|"EvalPHPArray")
   ;remove-rules-from-ruleset(|valid-name)
   ;remove-rules-from-ruleset(|"EvalPHPNextIndex")

  /**
   * Removes all rules from a given ruleset
   * @param name String the name of the dynamic rule
   * @type _ -> _
   */
  remove-rules-from-ruleset(|name) =
     keys := <dr-all-keys(|name)>
   ; <map({ key : ?key ; dr-undefine-rule(|name, key)})> keys