[Bug 5459] [FS] Static type analysis for the fn:abs, fn:ceiling, fn:floor, fn:round, and fn:round-half-to-even functions

tim@cbcl.co.uk changed:

           What    |Removed                     |Added
----------------------------------------------------------------------------
                 CC|                            |tim@cbcl.co.uk




------- Comment #11 from tim@cbcl.co.uk  2008-04-02 10:36 -------
We think we have a solution for min/max etc.  Here's the rules for min.  We
think the rules could be simplified, but as presented I hope it makes things
clear.

1. The simple case of the empty sequence.

statEnv |- Type = empty
------------------------------------------------
statEnv |-  (FN-URI,"min")(Type) : empty


2. Consider prime atomic types.  The set of types in T are those for which
ge(T, T) is defined.

statEnv |- Type2 = convert_untypedAtomic(Type, xs:double),
           Type2 <: T
           T in { xs:integer, xs:decimal, xs:float, xs:boolean,
                  xs:boolean, xs:string, 
                  xs:date, xs:time, xs:dateTime, 
                  xs:yearMonthDuration, xs:dayTimeDuration,
                  xs:anyURI }
------------------------------------------------
statEnv |-  (FN-URI,"min")(Type) : T


Rules for a union of prime atomic types.  

3. Rule for those types which are promotable to xs:double.

statEnv |- Type = (T1 | T2 ... Tn)
           (FN-URI,"min")(T1) : M1
           (FN-URI,"min")(T2) : M2 ...
           (FN-URI,"min")(Tn) : Mn
           M = (M1 | M2 | Mn)
           M <: (xs:integer | xs:decimal | xs:float  | xs:double)
------------------------------------------------
statEnv |-  (FN-URI,"min")(Type) : M


4. Rule for those types which are promotable to xs:string.

statEnv |- Type = (T1 | T2 ... Tn)
           (FN-URI,"min")(T1) : M1
           (FN-URI,"min")(T2) : M2 ...
           (FN-URI,"min")(Tn) : Mn
           M = (M1 | M2 | Mn)
           M <: (xs:anyURI | xs:string)
------------------------------------------------
statEnv |-  (FN-URI,"min")(Type) : M


5. Rule for the other permissable types.

statEnv |- Type = (T1 | T2 ... Tn)
           (FN-URI,"min")(T1) : M1
           (FN-URI,"min")(T2) : M2 ...
           (FN-URI,"min")(Tn) : Mn
           M = (M1 | M2 | Mn)
           M <: X in { xs:boolean, xs:date, xs:time, xs:dateTime,
xs:yearMonthDuration, xs:dayTimeDuration }
------------------------------------------------
statEnv |-  (FN-URI,"min")(Type) : X


6. Finally, sort out the quantifiers.

statEnv |-  quantifier(Type) in {1, +}
statEnv |-  (FN-URI,"min")(prime(Type)) : T
------------------------------------------------
statEnv |-  (FN-URI,"min")(Type) : T


statEnv |-  quantifier(Type) in {?, *}
statEnv |-  (FN-URI,"min")(prime(Type)) : T
------------------------------------------------
statEnv |-  (FN-URI,"min")(Type) : T?


The rules for "max" should be identical.  "avg" is slightly different in that
rule (2) must map xs:integer to xs:decimal, and the set of types in T are those
for which div(T, T) is defined (xs:integer, xs:decimal, xs:float, xs:double,
xs:yearMonthDuration, xs:dayTimeDuration).  Rule 4 would be ignored while in
rule 5, the set of types in X would modified ppropriately.

"sum" is slightly different again, in that rule (1) must reflect the fact the
the unary form of fn:sum returns xs;integer zero.  In rule (2), the set of
types in T are those for which plus(T, T) is defined (xs:integer, xs:decimal,
xs:float, xs:double, xs:yearMonthDuration, xs:dayTimeDuration).  I _think_ that
the binary form of fn:sum must consider the union of the types of the two
arguments.

Received on Friday, 4 April 2008 09:59:09 UTC