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

http://www.w3.org/Bugs/Public/show_bug.cgi?id=5459





--- Comment #15 from Michael Dyck <jmdyck@ibiblio.org>  2008-07-16 22:31:20 ---
Here's my proposal for abs/ceiling/floor/round/round-half-to-even. That's
FS 7.2.3, corresponding to F+O 6.4 "Functions on Numeric Values".  In the
above discussion, Comments #0, 2-3, 7-10, 13-14 deal with these functions.

One thing I realized was that semantics of these functions doesn't really
involve type promotion, so the invocation of "can be promoted to" is gone.
Also, I remembered that normalization does some of the work. And lastly, I
noticed we were ignoring the two-parameter version of round-half-to-even.

So, replace the whole of 7.2.3 / STA with the following text:

    Note that, in the declarations for the built-in functions fn:abs,
    fn:ceiling, fn:floor, fn:round, and fn:round-half-to-even, the (first)
    parameter is declared with type "numeric?". Thus, for a call to one of
    these functions, the normalization rules of 4.1.5 will have wrapped the
    argument in calls to fn:data() and fs:convert-simple-operand() (with a
    'prototypical value' of type xs:double).  Thus, static analysis of the
    call is guaranteed that the argument type is a subtype of
    xs:anyAtomicType*, with no occurrences of xs:untypedAtomic.

    In the static typing rule for these functions, we do a cardinality
    check on the argument type, extract its prime type (which must be a
    choice of atomic types), find the base numeric type for each, and then
    form the choice of those results.

        expanded-QName in { (FN-URI,"abs"), (FN-URI,"ceiling"), [etc] }
        statEnv |- Type1 <: xs:anyAtomicType ?
        prime(Type1) = AtomicTypeName1 | ... | AtomicTypeNameN
        AtomicTypeName1 has base numeric type AtomicTypeName1'
            ...
        AtomicTypeNameN has base numeric type AtomicTypeNameN'
        Type3 = AtomicTypeName1' | ... | AtomicTypeNameN'
        ------------------------------------------------------------
        statEnv |- expanded-QName(Type1) : Type3 · quantifier(Type1)

    The auxiliary judgment "has base numeric type" is defined as follows.

    If Type1 is (or is derived from) one of xs:integer, xs:float, or
    xs:double, then that is its base numeric type.

        Type2 in {xs:integer, xs:float, xs:double}
        Type1 <: Type2
        ------------------
        Type1 has base numeric type Type2

    Since xs:integer is a subtype of xs:decimal, we can't include xs:decimal
    in the above rule, otherwise subtypes of xs:integer would have both
    xs:integer and xs:decimal as their base numeric type. Instead,
    xs:decimal has its own rule, which excludes xs:integer and its subtypes.

        Type1 <: xs:decimal
        not( Type1 <: xs:integer )
        ------------------
        Type1 has base numeric type xs:decimal

    The fn:round-half-to-even function also has a two-parameter version.
    Its static type-checking can be reduced to that of the one-parameter
    version.

        expanded-QName = (FN-URI,"round-half-to-even")
        Type2 <: xs:integer
        statEnv |- expanded-QName(Type1) : Type3
        ------------------------------------------------------------
        statEnv |- expanded-QName(Type1, Type2) : Type3


-- 
Configure bugmail: http://www.w3.org/Bugs/Public/userprefs.cgi?tab=email
------- You are receiving this mail because: -------
You are the QA contact for the bug.

Received on Wednesday, 16 July 2008 22:31:54 UTC