[Bug 1705] [FS] technical: 5.2 Module Declaration: cyclical imports

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





------- Comment #37 from jmdyck@ibiblio.org  2006-11-04 08:57 -------
And while you're thinking about that, here's some other comments:

> Module1 ... Modulen reordered as Module1' ... Modulen'
> The order is such that variables in a module Modulei
> only depends on variables defined in Module1...Modulei-1.

That isn't quite what you want to say. First, it's the "primed" Modules that
satisfy the ordering constraint. Second, it doesn't allow variables in Modulei'
to depend on other variables in Modulei' itself, or on variables in Modules
other than the listed ones, both of which should be legal. Third, it ignores
functions depending on variables: if you try to do STA on a function body
before you have the type of a variable that it references, the STA fails.

So you could say:
    The order is such that variables and functions in module Modulei'
    don't depend on variables defined in Modulei+1'...Modulen'.

But it would be simpler to say
    The order is such that Modulei' does not depend on any of
    Modulei+1'...Modulen'.
Or equivalently,
    The order is such that if Modulei' depends on Modulej', then i >= j.

Yes, it's a slightly stronger constraint on the ordering, but the net effect is
the same, and since the non-circularity restriction is defined on the
Module-Module version of "depends on", it's easier to see that this version
(rather than the variables+functions version) of the ordering constraint is
guaranteed possible.

------

> AnyURI  is target namespace of modules Module1 ... Modulen
> Module1 ... Modulen reordered to Module1' ... Modulen'

You could merge these two judgments. Instead of introducing the "reordered to"
judgment, just say that the list of Modules "returned" by the "is target
namespace of" judgment is in the constrained order.

------

> Module1' = module namespace NCName1 = URILiteral; PrologDeclList1
> ...
> Modulen' = module namespace NCName1 = URILiteral; PrologDeclListn

The second NCName1 should be NCNamen, since sibling modules don't have to use
the same prefix for their target namespace. And the URILiterals should be
subscripted too, since those don't have to be exactly the same either (although
they do have to identify the same target namespace, of course).

------

> statEnv0 ; AnyURI |- declare namespace NCName = URILiteral;
>     PrologDeclList1 =>stat statEnv1 with PrologDeclList1'
>  ...
> statEnvn-1 ; AnyURI |- declare namespace NCName = URILiteral;
>     PrologDeclList1 =>stat statEnvn with PrologDeclList1'

In the last premise, the subscripts '1' should be 'n-1'.
Also, the NCNames and URILiterals should be subscripted.

------

> AnyURI =>module_statEnv statEnv
> statEnv extended with static environment statEnv1
>             yields statEnv1' for uri AnyURI
> ...
> statEnvn-1 extended with static environment statEnvn
>             yields statEnvn' for uri AnyURI
> ----------------------------------------------------------------
> statEnv |- import module AnyURI LocationHints? =>stat statEnvn

-- There aren't statEnv1 ... statEnvn any more.
-- You don't want to require that the statEnv returned by =>module_statEnv be
the same as the statEnv in the conclusion.
-- An AnyURI is not a URILiteral.

So that should be:

    URILiteral has atomic value AnyURI
    AnyURI =>module_statEnv statEnv2
    statEnv1 extended with static environment statEnv2
                yields statEnv3 for uri AnyURI
    ----------------------------------------------------------------
    statEnv1 |- import module URILiteral LocationHints? =>stat statEnv3

Received on Saturday, 4 November 2006 08:57:45 UTC