[Bug 1743] [FS] technical: 5.15 Function Declaration: a function can reference any function

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





------- Additional Comments From jmdyck@ibiblio.org  2005-09-02 00:52 -------
(In reply to comment #3)
> 
> Any comments on that plan?

I think it's a weak plan.  I realize that there are times when you have to
step outside the formalism and define something in prose, but I don't think
this is one of those times.

Making two passes over the Prolg doesn't seem that complex to me. Try this:

========================================================================
(1)

5 / STA / rule 1:

Take premise 1:

    statEnvDefault |- PrologDeclList =>stat statEnv with PrologDeclList1

and split it into 2 passes, yielding this rule:

    statEnvDefault |- PrologDeclList =>stat1 statEnv1
    statEnv1       |- PrologDeclList =>stat2 statEnv2 with PrologDeclList1
    statEnv2       |- [ QueryBody ]_Expr = Expr2
    statEnv2       |- Expr2 : Type
    -------------------------------
    PrologDeclList QueryBody : Type

========================================================================
(2)

Split 5 / SCP / rule 2 into the recursive rules for the two passes:

    statEnv  |- PrologDecl     =>stat1 statEnv1
    statEnv1 |- PrologDeclList =>stat1 statEnv2
    ------------------------------------------------------
    statEnv  |- PrologDecl; PrologDeclList =>stat1 statEnv2


                [ PrologDecl ]_PrologDecl = PrologDecl1
    statEnv  |- PrologDecl1    =>stat2 statEnv1
    statEnv1 |- PrologDeclList =>stat2 statEnv2 with PrologDeclList1
    ------------------------------------------------------
    statEnv  |- PrologDecl; PrologDeclList =>stat2 statEnv2
                                         with PrologDecl1 ; PrologDeclList1

And similarly for 5 / SCP / rule 1:

    -----------------------------
    statEnv |- () =>stat1 statEnv

    -------------------------------------
    statEnv |- () =>stat2 statEnv with ()

========================================================================
(3)
Define the "statEnv |- PrologDecl =>stat1 statEnv1" judgment...

(a) For PrologDecls other than VarDecl and FunctionDecl, simply
    take the existing =>stat rule and change '=>stat' to '=>stat1'.

(b) For VarDecls, it's a pass-through:

    ---------------------------------
    statEnv |- VarDecl =>stat1 statEnv

(c) For FunctionDecls, it only pulls out the function signature.
    Replace 5.15 / SCP / rule 1 with:

    [ FunctionDecl ]_FS = FunctionSignature
    statEnv |- QName of func expands to expanded-QName
    statEnv1 = statEnv + funcType(expanded-QName => FunctionSignature)
    ---------------------------------------
    statEnv |- FunctionDecl =>stat1 statEnv1

where []_FS adapts much of 5.15 / Normalization, but notably does not
involve []_Expr:

    [ declare function QName ( ParamList? ) ... ]_FS
    ==
    fn-sig ( [ ParamList? ]_ParamSig ) as item*

    [ declare function QName ( ParamList? ) as SequenceType ... ]_FS
    ==
    fn-sig ( [ ParamList? ]_ParamSig ) as SequenceType

    [ $ VarName                 ]_ParamSig == item*
    [ $ VarName as SequenceType ]_ParamSig == SequenceType

========================================================================
(4)
Define the "statEnv |- PrologDecl =>stat2 statEnv1" judgment...

(a) For PrologDecls other than VarDecl and FunctionDecl,
    it's a pass-through:

    not(PrologDecl is a VarDecl)
    not(PrologDecl is a FunctionDecl)
    ---------------------------------------
    statEnv |- PrologDecl =>stat2 statEnv

    (Or you can enumerate the cases if you like.)

(b) For VarDecls, take the rules of 5.14 / SCP and change '=>stat' to
    '=>stat2'.

(c) For FunctionDecls, take 5.15 / STA / rule (1|2) / conclusion, and
    change ": Typer" to "=>stat2 statEnv".

========================================================================

Received on Friday, 2 September 2005 00:52:08 UTC