5254 2007-11-06 10:48:15 +0000 [FS] Validate has inconsistent static and dynamic types 2009-02-16 07:42:50 +0000 1 1 1 Unclassified XPath / XQuery / XSLT Formal Semantics 1.0 Recommendation PC Windows XP CLOSED FIXED P2 normal --- 1 nick jmdyck public-qt-comments oldest_to_newest 17606 0 nick 2007-11-06 10:48:15 +0000 In FS 4.13 the static type analysis for validate expressions can only ever be a union of element types. But in FS 4.13.2 the validate expression can yield a document rather than an element. I think the fix would be to split the static type analysis rule into two. One for elements, the other for documents. statEnv |- Expr : Type statEnv |- Type <: (element) statEnv |- prime(Type) = ElementType1 | ... | ElementTypen . (same as current rule) . statEnv |- validate ValidationMode { Expr } : Type1 statEnv |- Expr : Type statEnv |- Type <: (document {ElementType}) statEnv |- prime(ElementType) = ElementType1 | ... | ElementTypen . (same as current rule) . statEnv |- validate ValidationMode { Expr } : document {Type1} 18407 1 jmdyck 2008-01-18 06:54:31 +0000 I agree that there's a problem, and I agree with your approach to a solution. However, the original rule has some additional bugs that also need to be fixed: 1. The type 'element' should be 'element *'. (See Bug 3269.) 2. The earlier and later occurrences of ElementTypei should be distinct. 3. Requiring Type <: document { ElementType } is too restrictive, because ElementType cannot be bound to a type involving (a) processing-instruction or comment types, or (b) a union of element types. Points 1, 2, and 3a are all easy to fix, but I'm not sure what to do about 3b. 18454 2 nick 2008-01-22 13:06:21 +0000 > 3. Requiring Type <: document { ElementType } is too restrictive, because > ElementType cannot be bound to a type involving > (a) processing-instruction or comment types, or > (b) a union of element types. > I think "ElementType" isn't actually an ElementType, it was just an unfortunately chosen name. If it is changed to "Type_Element" or something then I think the rule is valid. The prime(Type_Element) = ElementType1 | .... | ElementTypen should cover the union case. 18460 3 jmdyck 2008-01-22 18:02:02 +0000 (In reply to comment #2) > I think "ElementType" isn't actually an ElementType, it was just an > unfortunately chosen name. That could be, though I somewhat doubt it. > If it is changed to "Type_Element" or something then I think > the rule is valid. > > The prime(Type_Element) = ElementType1 | .... | ElementTypen should cover the > union case. But then: 1) It incorrectly allows multiple elements in the document content. 2) It doesn't allow processing-instructions or comments. 3) Given a binding for Type_Element that satisfies the rule, there are (infinitely?) many supertypes of it (and possibly some subtypes of it) that also satisfy the rule, and that lead to different types for the validate expression. 23363 4 jmdyck 2009-02-01 00:31:14 +0000 It occurred to me that splitting FS 4.13 / STA / rule 1 into a rule for Type <: element and a rule for Type <: document { ... } woldn't allow for a Type that was a union of (subtypes of) those two possibilities. After some thought, I'm instead proposing to replace that rule with the following set of rules (leaving out "statEnv |-" here for brevity), which I think handle all problems raised above. Expr : Type Type <: element * | document { element * & (processing-instruction * | comment)* } Type with mode ValidationMode unites to TypeU ---------------------------------------------------- validate ValidationMode { Expr } : TypeU prime( Type ) = FormalItemType1 | ... | FormalItemTypen FormalItemType1 with mode ValidationMode resolves to FormalItemType1' ... FormalItemTypen with mode ValidationMode resolves to FormalItemTypen' FormalItemType1' | ... | FormalItemTypen' = TypeU ---------------------------------------------- Type with mode ValidationMode unites to TypeU DocumentType = document { Type } Type with mode ValidationMode unites to TypeU ---------------------------------------------------- DocumentType with mode ValidationMode resolves to document { TypeU } ElementType = element ElementNameOrWildcard OptTypeSpecifier ElementNameOrWildcard with mode ValidationMode resolves to ElementType' ---------------------------------------------------- ElementType with mode ValidationMode resolves to ElementType' ---------------------------------------------------- ProcessingInstructionType with mode ValidationMode resolves to none ---------------------------------------------------- comment with mode ValidationMode resolves to none 23381 5 nick 2009-02-02 11:06:19 +0000 That looks good to me, so I'm happy to close if no one else has a problem with it. 23388 6 jmdyck 2009-02-02 18:58:23 +0000 Well, it would need to be approved by the WG first. 23433 7 jmdyck 2009-02-04 06:44:32 +0000 At their joint meeting this morning, the XQuery and XSL WGs approved the proposal in comment #4. Consequently I'm marking this issue resolved-FIXED. Since you have already expressed your approval of the proposal, I will also take the liberty of closing the issue. 23761 8 jmdyck 2009-02-16 07:42:50 +0000 This issue has been entered as FS erratum E058, and the proposed fixes have been committed to the source files for the next edition of the FS document. (Mind you, I made some editorial changes to the new judgment forms, to reduce confusion with the judgment defined in 8.6.1.)