04. Grammar言語

共通parserの各arenaは、操作内で受理したsource/map列の取込位置をprivate状態として保持できる。 受理列は成功したtoken読取り間でprefixを保持し、arenaへは未取込suffixだけを検査・追加する。 Foreign arenaは独立した取込位置から開始し、host復帰後も必要なsource/mapを保持する。 外部ParseProgressのechoからこの位置を構築せず、別revisionの再解析では新しい状態から開始する。

方針

Grammarはreader・prefix形状・束縛・表示の定義を同じpackageへまとめる。任意プログラムを小さなGrammar IRへ必ず還元することは要求しない。call/map/thenで登録済みproviderへ委譲できる。

1. 文書の根と名前解決

根は language name revision root declarations。declarationsはcons/nil列。全constructorは grammar-signatures.md に定義する。宣言の順番はmetadata解決に影響しない。category/mode/reader/namespace/extension aliasの各名前空間で同名を拒否し、参照先をcompile時に解決する。formとleafの宣言はそれぞれcategoryとkindの組で一意とする。

一つのkindを複数categoryで受け入れることは、field schemaが完全に一致する場合に限り許可する。grammar自身のField宣言とSelectorのfield等、同じ綴りでshapeが異なる場合は異なるkind IDを付ける。modeごとのspellingとschema kindを混同しない。

共有kindのsurface descriptorは一つであり、categoryごとのbinding/style/read宣言は別に保持する。DeclarationOriginはform/leafに限ってcategoryを持ち、同じkind名の各宣言位置を区別する。その他の宣言のcategoryはNoneである。この出自の区別はexecution identityへ含め、意味上の宣言順序は引き続き無関係とする。

builtin Name/Text/Nat/Lang は配布された基礎readerを直接参照する。local C は現在言語のcategory。foreign Alias C はprofileで固定した別schemaのcategory。withmode M R はその引数だけのmode切替え。listof R は専用list categoryを特殊化し、cons/nilの既知shapeへ展開する。

foreign aliasはpackage sourceからURLをfetchして解決しない。profile manifestのSchemaRefを要求し、未登録はMissingLanguage、digest不一致はSchemaMismatch。

2. formとleaf

form Kind Category "spelling" fields binding styles。 fieldsの長さがarity。各field名はform内で一意。head自体はfieldでない。source範囲は共通parserが記録する。

leaf Kind Category TokenKind binding styles。 明示的なtoken kindだけをarity 0として受け入れる。Category内の既知formのspellingとの照合を先に行う。形状に一致しないWordを参照leafとして受け取るかは、そのCategoryのleaf宣言に従う。

読み取っただけではdomainの評価器を呼ばない。compileはGrammarの意味操作として明示的に呼ぶ。

3. 束縛plan

planはsource fieldとscopeの関係を記述する。評価順やメモリへの代入命令ではない。

none: このnode自身は何も追加しない。記述し忘れを隠すために子を自動visitしない。fieldのうち語義解析不要のliteral以外には、visit/import/propagate/専用plan/customのいずれかで処理方針が必要。

visit field: 現在scopeでその子のplanを適用。子内部のscopeは外へ漏れない。 group plans: 現在scopeを使ってplanをまとめる。 scope plans: 子scopeを作ってplanを適用。bindの位置より後のvisitだけに新しい宣言を見せる。 bind namespace field: 一つの名前fieldから新しいEntityを導入。名前を作れるfieldはbuiltin Name/Textか、schemaでTextを返すと検査されたleaf。Textのescapeはdecode後の綴りで比較し、元位置はSourceMapで保持する。一般の式を名前に変換しない。 reference namespace field: 名前field(leafではself)を現在scopeに対する参照として登録。 export namespace field: 名前を導入候補として親へ返す。単独ではglobal scopeを変更しない。 import field: 子がexportした候補を現在scopeへ導入。 propagate field: 子のexportをこのnodeのexportとして返す。child内の参照も、そのchildに割り当てたscopeで登録する。 sequential declarations body: 各宣言を、それ以前のexportだけが見えるscopeで処理し、そのexportを追加した新しいscopeで次へ進む。最後のscopeでbodyを処理。 recursive declarations body: 各宣言のexport headerを先に収集して共通scopeへ導入し、全宣言の本体とbodyをそのscopeで処理。 custom provider: 同じScope/Entity/Occurrence/Relation契約を返す専用処理。providerの出力も範囲・ID・scope edgeを検査する。

二相処理として、scopeと宣言を作り、参照を後で解決してよい。ただし上記の可視性を変えない。scope graphは有限。候補が複数ならAmbiguousを返し、最初に見つかった候補へ勝手に決定しない。

lexical namespaceは内側scope優先。openは同じlexical探索を行い、見つからない名前を自由入力要求として返す(架空の定義位置を作らない)。globalは指定されたroot scope内で同名の重複を拒否する。別articleのDocLabelや別moduleのSignalを同じglobalへ入れない。rootの割当てはそのform/packageのplanまたはfacts providerが指定する。

Foreignの既定は、各foreign bundleへ独立したscope rootとnamespace instanceを割り当てることである。同じsurface schema、alias、同言語への再帰であっても外側rootを暗黙に共有しない。同じschema/nameでもrootが異なれば別NamespaceRefとなる。外側の名前・候補を渡す場合は明示EnvironmentProjectionおよびroot/namespaceのprojection・grantに従い、外側の既存scopeへ書き込む権限を読み取り候補の共有から推定しない。import/propagateで渡すexport候補も、その明示した名前空間の対応に従う。foreignの局所NodeRef/OriginRefは所属bundleに対して解決してからanalysisの共通tableへ再配置する。

3.1 宣言順と解析結果の境界

BindingStageはScopeId、previous、introduced EntityId列を保持し、StageIdはその解析のstage表に対するindexである。previousは必ず以前のstageを指し、同じscopeの以前の可視性、またはscope作成時に捕捉した直接親scopeの可視性を表す。同じlexical scopeのstageを新たなscopeとして扱わず、そのscopeの可視候補を集めてから外側scopeを探索する。同じscopeで同名の異なるEntityが見える場合、最後のstageの一件だけを選ばない。sequentialが要求する新しいscopeは別ScopeIdを作る。

初期root、namespace instance、Origin閉包の割当てはhost bundleを先頭とし、正準node/fieldのDFS順でForeign bundleを訪問して行う。各bundleの選択も正準node順で扱い、source表はSourceId/revision/digest順にする。入力のcontexts列やselection列の格納順からFactSetのIDを割り当てない。同じanalysis IDとAnalysisKeyでnative実行と正準treeの受信後実行を行う場合、生成Entity/Occurrence/ScopeのIDが異なる対象を指してはならない。既存opaque facts IDをtreeのnode IDと一緒に再採番する規則ではない。

OccurrenceStageはDefinition/Reference/Import/Exportの各Occurrenceと、発行時のstageを対応させる。完成結果では全Occurrenceにちょうど一つの対応が必要であり、途中結果でもOccurrenceと対応の片方だけを公開しない。visitは受け取った可視性から子のplanを実行し、子の変更を親のstageへ暗黙に反映しない。親への導入はimport、親への候補返却はexport/propagateの実行規則に従う。stage内のEntityIdが存在することだけでは、そのEntityを導入する意味的権限を証明しない。

Occurrence.scopeとOccurrenceStage.stageは名前が現れたlexical scopeとその履歴を保持する。OccurrenceStage.namespaceStageは検索対象の履歴を別に保持し、Lexical/Openではstageと等しく、Globalではそのnamespaceの指定rootに属する発行時のstageを指す。GlobalのEntityは指定rootへ配置するが、Occurrenceのlexical位置をrootへ置換しない。Globalへのbindと明示importはrootの可視履歴を更新し、lexical scopeを出た後の兄弟からも既に導入した宣言を検索できる。exportによる候補作成だけでは更新しない。明示recursiveのheader収集を除き、後続宣言を過去の参照へ可視にせず、同じroot内の同名導入はDuplicateGlobalと位置診断で拒否する。別Foreign bundleのrootへ暗黙に導入しない。

portableの構造検査はnamespaceStageの存在、namespace policyとの組合せとroot所属を検査する。そのstageが実際の参照時点の最新履歴だったことや、候補を導入する権限は型付き値だけでは証明せず、実plan実行の意味proofに属する。

engineのBindingAnalysisは実BindingPlanの完走と名前解決により得る意味proofであり、共通CheckedFactSetの型・ID・参照・source検査と区別する。入力treeの各selectionは同じ解決済みProfileのexecution identityへ再照合し、意味identityが等しい別arena配置を代入しない。完成結果は必須FactSet、stage列、OccurrenceStage列、open入力のOccurrenceId列、export候補EntityId列、Report用source/mapsを保持する。公開schemaの同じrecordを受信しただけでnativeの意味proofを生成しない。

BindingBundleScopeは解析入力treeの正準bundle番号と、その準備時に実際に発行したroot ScopeIdを結び付ける。ScopeIdの数値をbundle番号やarena indexから推定しない。BindingProgress/BindingAnalysisのbundleScopes列は正準bundle順の初期化済みprefixを保持し、各scopeは存在する異なるrootでなければならない。停止前に発行したscope/stageは保持し、未公開の対応行を捏造しない。完了した意味proofの対応は全bundleを覆う。raw返信だけでは入力treeのbundle数や実際の発行関係を認証できないため、prefix・参照・root・重複の構造検査を、同AnalysisKeyの実Binding完了proofとの照合の代わりにしない。

各対応行のcustomSourceMapsは、同じBindingProgress/BindingAnalysisのsourceMaps表でCustomが正式受理した行のindex列である。呼出対象のbundleを所有者とし、FactsEmitterの受理時と検査済みFactDeltaのsource閉包受理時にmapと所有indexを同時に公開する。後の停止や意味拒否でも受理済み両列を保持する。indexは所有列内で狭義昇順、表の範囲内、所有列をまたいで重複しない。同じ内容のmapを別bundleが明示的に返した場合は別の受理行として保持し、内容一致から所有者を推測しない。元treeのmapは引き続き各SyntaxBundleの局所表を用いる。raw列の構造検査はCustom呼出の真正性や授権の証明ではない。

BindingReplyは共通Reportを持ち、Complete、Invalid、Stoppedの全枝がsource/mapsを所有する。途中BindingProgressはfacts:Option<FactSet>で初期化前を区別し、その場合も受け入れたsource/mapsを保持する。空のanalysis identityを持つ偽FactSetで停止を表さない。Someの部分FactSetは共通の構造不変条件を満たす必要があるが、plan完走や名前解決の完了を主張しない。InvalidのBindingFailureは、Tree/Profile/Package/Planおよび共通Fact/Source/Schema/Origin/View/Syntaxの入れ子原因と引数を型付きで保持する。SourceError.DecodeのvalidUpTo/errorLenも失わず、粗いTree/Source分類やDebug文字列でnativeとの違いを隠さない。UndefinedName、AmbiguousName、DuplicateDefinition等の語彙診断はBindingDiagnosticArguments(namespace, name)と実source位置を持つ通常Diagnosticとして返す。

停止の分類は型付き原因をたどって決める。SyntaxのSource/View/Schema等の内部にStoppedがある場合も元StopReasonをBindingOutcome.Stoppedへ伝え、Invalidへ変えない。逆に、別の処理でBudgetが停止済みであることだけを理由にWrongTypeやBounds等の意味失敗を上書きしない。単独のBindingFailure codecは停止原因もデータとして保存できるが、BindingReplyのInvalidにStopped原因を含めることは拒否する。traceOverflowもStoppedのReportだけが持てる。

初回BindingReply decoderは、受信したFactSetとReport用source/mapsから閉包を構成し、元のRust結果やambient SourceStoreを要求しない。各source表内の重複を拒否し、表間で同じsnapshotを共有する場合はbytes/digest/URIの一致を要求する。stageの後方参照、scope親子、全Occurrenceとの一対一対応、open入力とexportのIDも検査する。これは構造上の結果交換であり、通信認証、元tree/Profileへの要求identity照合、名前解決の再実行を代わりに証明しない。schemaのBindingAnalysis recordはnativeの公開raw BindingResultに対応し、private BindingAnalysis proofは実analyzeからのみ得る。

Custom の native 実行と解決更新履歴

analyze_with_host は選択済み provider requirement と明示した呼出先に対して host が発行した FactAuthority を検査し、同じ既存facts・treeを借用する CheckedFactsView を callback へ渡す。owned FactsRequest と借用viewは同じvalidatorに従い、通常のnative呼出しのためだけにtreeと全factsをNDFへ複製しない。hostは登録済み実装のrevision・digest・operationを照合する。未登録はMissingProviderであり、providerの自己申告から変更権限を得ない。

native callbackの診断・eventは FactsEmitter によってsource/map・schema・Fix・件数を検査した時点で正式collectorへ追加する。戻り値の CustomOutcome は Complete(delta)、Invalid(partial)、Stopped(reason, partial) を区別する。deltaの参照・予約ID・namespace/root・変更権限を検査し、必要storageを準備した後に原子的に適用する。停止した親Budgetへ新しいraw deltaを無検査で追加せず、既に受理した診断・event・sources/mapsを残す。外部FactsReplyのdecodeとremote実費の精算はこのnative emitterを呼んだだけで成立したことにはならない。

Customの明示resolution updateはOccurrenceの位置・scope・発行時stage・namespaceStageを書き換えない。BindingResolutionBatchは選択provider、発行authority、解析要求内の正準path/nodeで表したtarget、OccurrenceIdごとのbefore/after列を保持する。delta適用と履歴追加は一つのcommitとし、同じOccurrenceへの更新は前のafterと次のbeforeが一致し、最後のafterがFactSetの確定resolutionと一致しなければならない。疎なEntity/Occurrence等のIDをarena indexとして解釈しない。Custom解決を通常のlexical lookupの結果と偽って扱わない。

raw BindingReply codecは履歴の型、既存ID/namespace、authorityの参照・scope範囲、明示resolution grant、before/afterの構造、更新の連鎖と最終結果を検査する。履歴authorityに記録した予約範囲が過去の発行時に空いていた事実、最初のbeforeの真実性、providerが実行された事実、外側要求がない場合の正準targetの所有者をraw返信だけから認証しない。元要求・選択Profileに結び付いた実実行が意味proofの根拠である。

FactsRequestのphaseはOrdinary、Header(group)、Body(header)を区別する。recursiveは全宣言のHeaderを収集してexport候補を導入した後に各Bodyを実行する。HeaderのFactDeltaは新しい宣言Entityと明示Export occurrenceを返し、Reference occurrenceと既存resolution更新は返さない。初期化式の参照検査は全headerが揃ったBodyで行う。Headerで省略したvisit/import先のCustomは、BodyでOrdinaryとして実行する。propagateで実際にheaderを訪れた宣言は対応するBodyを実行する。

FactsHeaderはgroup、選択済ProviderRequirement、要求内の正準path/nodeで表したtarget、受理したentitiesとexportsのID列を持つ。exportsはこのheaderで受理したentitiesの重複しない部分列である。native機械はrecursive group、実target、BindingIdごとの受理順にprivate memoを保存し、各headerを一つのBodyへ対応させる。同じplanを別groupで実行した場合や同じtargetを繰り返し訪れた場合にmemoを共有しない。Bodyは既存header IDを参照し、runtimeはそのexport候補を再利用する。既存IDをdelta.entitiesへ再追加する操作はDuplicateIdとして拒否する。新しい予約IDの別宣言を、名前・Span・scopeの一致だけでheader再発行と推測して拒否しない。同名の別Entityは通常の可視性とAmbiguousの規則に従う。

raw phase検査ではgroupがauthority.currentScopeの祖先(自身を含む)であること、Bodyのprovider選択・Facts署名、targetの正準座標、既存Entity参照、ID列の重複とexports包含を検査する。別Foreign rootのgroupを流用しない。ただしraw FactSetだけではscopeと解析対象の実行履歴を認証できない。受信したreceiptを自己申告の実行proofへ昇格させず、hostの授権とnativeの保存memoへ束縛する。replyもHeaderの制約と発行したauthorityへ照合してから適用する。

実装試験は通常Custom、recursive Header/Body、独立Foreign root、停止時の正式collector保持、同じcallbackへの実NDF/CBOR初回受信とnativeの結果比較を含む。同期codec処理は親のBudgetとSourceAdmissionを共有する。別processへのFacts quota貸出・実費精算は引き続き別実装項目であり、この同期比較を外部processの費用保証と扱わない。

4. 非再帰letの完全な規則例

form Let Expr "let"
  cons field name builtin Name
  cons field init local Expr
  cons field body local Expr
  nil
  group
    cons visit init
    cons scope
      cons bind Value name
      cons visit body
      nil
    nil
  cons style head "marker"
  cons style field name "name.definition"
  nil

lambdaはparameter/bodyの2fieldとbodyだけのscope。letrecは同じnameをinit/body双方のscopeへ導入する。letrecの名前解決成功は初期化の妥当性や停止性を意味しない。

5. style

style selector class-nameを登録する。head/self/field/captureからsource領域を選ぶ。captureはreaderが宣言したcapture名。未定義field/captureはcompile error。

同じGrammar/Style列に selection selector priority を宣言できる。selectorはstyleと同じhead/self/field/captureで、priorityはNatから損失なく変換できるU64とする。省略したselectorのpriorityは0であり、同じownerの同一selectorへのselection重複は拒否する。範囲の大小が第一条件で、同じ範囲長の候補は大きいpriority、深い包含位置、宣言順の順で選ぶ。styleの既存arityを変更せず、classと優先度を別の列として保持する。

LanguagePackageのForm/Leafおよび動的HeadShapeは SelectionRule { selector, priority } の順序付き列を持つ。実Grammar compilerがこの列を生成し、package意味identityと選択Profileのexecution identityへ含める。未定義field/capture、重複selector、U64上限を超えるNatは元operandまたは重複宣言の位置を持つ失敗として返す。priorityをnative arena配置から推定しない。

class名はschema所有ID。共通roleへfallbackできる。実際の色をgrammarに固定しない。binding metadataからdefinition/reference修飾を自動で導出する。

6. compileの出力と検査

compileは LanguagePackage{schema, readerPlans, categoryShapes, bindingPlans, stylePlans, extensionRequirements, provenance} を返す。意味データに加えてどのgrammar宣言から作ったかを保持し、grammar自身にもdefinition jumpを提供する。

ここでschemaはsurface schemaであり、Doc:Sentence等の意味schemaと区別する。標準profileは nepl3.syntax.grammarnepl3.syntax.docnepl3.syntax.mathnepl3.syntax.circuit をsurfaceの所有packageとし、意味packageはそれぞれ nepl3.grammarnepl3.docnepl3.mathnepl3.circuit に分ける。LanguagePackageはpayloadSchemasとして必要な意味・provider schemaの実SchemaRefも宣言する。sourceのform名・token名・view名を同一descriptorで衝突させず、compiled metadataでそれぞれのkind identityへの対応を持つ。

SyntaxNode.schemaとForeignSyntax.schemaは該当するsurface schemaを指す。Token.kindはWord等のlexical分類なので、Let等のSyntaxNode.kindと同一であるとは限らない。form/leaf宣言が両者の対応とpayload型を定める。SentenceLiteralの外側shapeはarity 0のまま、Token.payloadに入るDoc:Sentenceは意味schemaを指す。engineはsurface構造とpayloadの宣言型を照合するが、読むだけで意味操作を実行しない。

sourceから読むarity 0のleaf(builtin Name/Text/Nat等も含む)はfields=[]とし、値はnode.tokenが指すToken.payloadだけに所有する。builtin引数を親formのAtomへ直接縮約せず、token/head/cover/Originを持つliteral child nodeとして保持する。leafのsurface descriptorは空record、token descriptorのpayload fieldが実際の値型を宣言する。Binding/Styleのfield selectorは該当childのtokenとSourceMapを明示的にたどる。source-lessの意味constructor/printerはdomain意味モデルで提供し、架空のToken.head/Spanで生成構文を埋めない。

surface descriptorの型名はForm:/Token:/View:/Builtin:等の役割を持つ名前空間で分け、同じsource kind名に異なるfield shapeを割り当てない。LanguagePackageの意味identityはsurface SchemaRef.digestとは別で、reader/mode/binding/style/extension等の実行metadataを含める。名前で参照する宣言の順序は除き、skip/take/choice/field/binding列の意味順を保存する。readerの直接ReaderId edgeはpackage内ではDAGとし、再帰は名前付きRefで表す。これは完全Grammar構文の有限ReaderExprと一致する。standalone ReaderPlanの直接cycleとは区別し、rule名順の根からDAGを展開する正準形によって共有・同じ式の複製・arena配置の違いを除く。Refは名前を保持するため再帰の正準形も有限である。

extension requirementは既知の型付きoperation descriptorと署名を照合するが、実行callbackの登録とは別である。name-v1/trivia-v1のreader/v1 adapterはReadRequestを受け、対応するbuiltinを予約なしで実行してReadReplyを返す。予約を持つBuiltinRequestとreader/v1を暗黙互換にはしない。Text builtinは明示した予約付き入口を使う。facts/v1等のcustom bindingもparse/compileだけで自動実行せず、実行操作をhostが選んだ時にcallback未登録ならMissingProviderで拒否する。compiler自身の宣言名・selector検査をfacts callbackへ丸投げしない。

facts/v1の署名は純粋なnepl3.engine.FactsRequest→FactsReplyとする。要求はParseTree内の明示path/node、既存FactSetとhostが与えたFactAuthorityを保持する。CompleteはFactDelta、Invalid/Stoppedは任意のpartial deltaとReportを返す。全枝はReport専用のsources/sourceMapsも所有し、partial=Noneでも生成source上の診断を失わない。この表はdeltaのfacts追加と独立であり、診断のためだけに仮deltaを作らない。Reportの参照は要求のtree内各局所source表・既存FactSet・返却delta・明示Report用source表を合わせて解決し、hostの無関係なglobal storeで欠落を補わない。独立表に同じsnapshotを含む場合はidentity/URIの一致を要求し、SourceAdmissionは同じ操作内で一度だけ計上する。

共通facts値の所有・検査はnepl3.core、解析treeを含む包絡はengineが所有する。標準catalogは実descriptorを登録して宣言を照合する。FactsRequest/Replyの型付きadapterはengineからcore-owned FoundationValueCodecを介してwireの実FactSet/Delta/Report変換を使い、wireからengineへの依存は追加しない。sourceMapsの要素はSourceMappingであり、mappings列をさらに持つSourceMapレコードではない。空列では区別できなかった旧FactsReply schemaのList<SourceMap>を、生成sourceと実mapを含む往復試験に合わせて訂正した。

hostは自ら選んだ要求をFactsRequest.issueで検査し、変更不能な元要求と解決済みProfileを借用するCheckedFactsRequestを発行する。これは外部から受信したauthorityの自己申告を認証する入口ではない。初回受信のrequest_decodeは元Rust要求を持たずに明示wire表から型・参照・source・tree・authority参照の不変条件を検査し、raw FactsRequestを返す。授権proofは返さず、受信hostがtransport認証と操作許可を確認した後だけissueを呼ぶ。未認証・未許可の受信requestからproofを発行してはならない。

別途request_from_valueは送信側のecho/loopback検査であり、保存された元要求のproofを要求する。tree/path/nodeの正準番号への変換後、要求全体の型付き値を予算付きで照合する。analysis identity、既存facts、全namespace・writable/import scope・resolution/relation grant・ID予約も一致対象である。初回受信とこの完全一致検査を混同しない。独立process間の通信認証と実行授権はhost transportの責務である。

返信deltaは保存された元要求のexisting/authorityに対して検査し、返信から権限を得ない。Invalid/Stoppedのpartial=Noneでも、treeの全foreign bundle・既存facts・任意delta・Report専用source表のidentity/URI整合とmap閉包を検査する。Reportのprimary/related/fix/eventはこの明示閉包へ限定する。Report.usageの内部件数整合と、遠隔処理の実消費量の認証・共有Budgetへの吸収は別であり、codecは申告Usageを自動加算しない。この実装は静的ParseTreeと共通factsの構造・権限境界の証拠であり、facts callbackや語彙scope解決アルゴリズムの実行、Dynamic tree、全providerのprocess比較の完成を意味しない。

名前のbinding selectorが読むleaf payloadはTextでなければならない。seqはListを返し、名前への暗黙の文字列連結は行わない。正式binding例のNameは標準name-v1操作を明示してTextを得る。名前として使用しないNumber readerのList<Text>出力はそのまま保持する。payloadSchemasは実際のreader型、token payload、view/style、extension操作が参照する型定義の閉包から集め、未使用のregistry登録を依存へ含めない。

解決済みProfileはsurface、意味、reader/providerの全descriptorと計算済みdigestを登録する。未生成のpackageへ架空のdigestを置かず、同じSchemaRefに異なるfield shapeを割り当てない。Grammar compileはsurface descriptorを作る責務を持ち、Doc/Math/Circuitの意味schemaを勝手に再生成・上書きしない。

必須検査: 未定義category/mode/reader/namespace/provider、重複kind/field/spelling、field型の不一致、readerの空反復、進捗なし再帰、未読fieldへの構文context依存、bindingで非名前fieldを使用、範囲外のstyle selector、foreign alias不足、provider署名不一致。

Grammarが生成したdescriptorと、同じ契約をRustで直接構築したdescriptorは同じengineで動く。埋め込まれたproviderをdescriptorの固定IRへ変換できなくても、その呼出し参照を保持する。

7. 構文環境を更新する宣言

通常のvalue bindingは名前解決環境だけを変える。関数値をbindしたからといって、その名前のarityを自動変更しない。

外部HeadProviderは shape(head, existingContext)context_for_child(head, index, completedChildren) を提供できる。後者は既に読了した子だけを参照する。schemaを変更する宣言の作用範囲は、その宣言が導入したbodyの部分木とし、復帰時に元へ戻す。

動的操作の共通要求はHeadCall、返信はHeadReplyとする。要求にはsession/call/operation/Profile/execution identity、EntryContext、環境のopaque参照、既読headとShapeまたはChildContextの種別を保持する。既知のstatic spellingが最優先で、その次に当該alias/categoryのshapeを呼び、Shape(None)のときだけleaf候補へ進む。固定shapeのfieldsがarityを定め、child iへの要求はそれより前に読了したi個のrootだけを順に保持する。childContext返信は登録済みEntryContextを選び、固定field数やNodeRef/ForeignSyntaxのslot形状を変更しない。

投影は完全SourceSnapshotを含まず、ProjectedSpan(source,start,end)と、その範囲のUTF-8 bytesを持つSourceWindowを使う。これはcore Spanと別の位置型であり、部分bytesだけから元全文digestの正しさを証明しない。hostは元snapshotから窓を捕捉して発行callに束縛し、受信側は窓内の相対UTF-8境界・長さ・参照整合を検査する。ProjectedSyntaxはforeignも含む独立flat node arenaを持つ。元bundleのEnvironmentRefはopaque metadataで、投影全体の環境表をlookupする権限ではない。

既読Token.payloadはcompoundを含むNdfValueを保持する。その意味値にSourceContent等の形をしたrecordが含まれても、自動source解決・admission・環境権限へ昇格しない。parser自身が未読child、未消費source bytes、Originや環境resourceの自動閉包を追加提供しないことが投影の契約であり、任意readerがpayloadへ何を書くかまで含む完全な情報非干渉の証明ではない。

HeadReplyは新sourceを生成しない。ProjectedReportの位置だけをProjectedSpanで表し、hostが保存windowへの包含を照合して元snapshotから通常Spanへ復元する。primary/related/fix/eventを同じ窓へ限定し、型・Fix期待digest・編集非重複・同一SourceIdの前提revision・Report件数等は共通Report検査を使う。部分sourceから短縮SourceSnapshotや未検査Spanを作らない。HeadContinuationはparserの進捗と待機tokenを所有するhost側の継続であり、providerへ渡すのはHeadCallだけである。

native resume_headのcaller SourceStoreは元の主入力snapshotを解決し、保存済みidentity・内容・URIと一致しなければならない。欠落・不一致は待機要求を消費しない。補助・生成sourceは保存済み閉包を利用でき、caller storeへの全件再登録は要求しない。返信Reportは保存された明示窓と宣言source閉包の規則で検査する。

今回の配布4言語はschemaをソース本体の途中で自己変更しない。Grammar sourceをcompileして別の入力に適用する順序を標準経路にする。動的HeadProvider経路は契約試験用の局所構文例で実装・検証する。単にAPIだけ残して未実装にしない。

永続する解析選択と検査範囲

ParseTreeはProfile digest、SyntaxBundle、bundleごとのNodeSelectionとRecoveryEntryを保持する。foreignへのpathの各NodeRefはその段階の所有bundleに属し、field名で次のForeignSyntaxを選ぶ。各到達nodeには選択がちょうど一つ必要で、static form/leaf/readのindexはEntryContextのaliasとpackage executionDigestで所有を固定する。既知formの原文spellingをleafへ付け替えてarityを変えたり、親ReadSpecと異なるalias/category/modeの子を置いたりしてはならない。ListOfのtailは同じspineのcontextとReadSpecを保持する。

Dynamicの完成選択は固定HeadShape、providerの操作参照、field順のchildContextsを保存する。childContextsは完成treeではfieldsと同数であり、各実childの選択と一致する。callbackは固定arityやNodeRef/ForeignSyntaxのslot形状を変更できず、解決済みProfileの実package/aliasからcontextを選ぶ。進行中frameは既読または開始済みchildまでの確定prefixを保持し、完成treeと同じ完全性条件を先取りしない。

HeadCallの初回portable受信は元Rust要求や全文SourceStoreを前提にしない。ProjectedSpanはsnapshotに対する絶対byte範囲であり、受信側は窓内の相対位置を使ってUTF-8境界を検査する。同じSourceId/revisionに異なるdigestを宣言できず、同一SourceRefの重なる窓は共通区間のbytesが一致しなければならない。flat projected arenaの全参照・root数・schema field形状・到達性・循環と、全位置の窓閉包を検査する。coverの元入力への忠実性と全文digestの認証は、この内部整合検査からは証明されない。既読payloadをsource検索権限へ昇格させず、窓を短縮SourceSnapshotとして登録しない。

遠隔費用を扱う包絡はHeadDelegation(call, limits)とHeadDelivery(reply, usage)とする。HeadCallのnative意味を変更せず、hostは保存した発行callの全窓を実snapshotと照合し共有SourceAdmissionへ全文をonce計上した後、非公開の発行proofに親Limits・累積Usage基準を固定し、親Budgetを排他的に借用する。子のSourceBytes上限は発行窓の区間unionであり、親の未使用SourceBytesではない。その他の加算資源は親の残余からhostが明示した送受信・検査用reserveを差し引いて貸し出す。予約容量を実消費Usageへ記録しない。Depthは親の絶対上限とHeadCall.depthBaseを用いる。受信窓ledgerはその子操作だけに属し、重複・包含・交差する同一snapshot区間をonce計上する。

親のNDF変換・実wireエンコード・返信デコードは発行proofのtransport入口で実行し、貸出分を除いた一時ceiling内で処理前に計上する。reserveを超えれば停止し、Resultの成功・失敗にかかわらず外側Limitsへ復帰するが停止理由は維持する。子側の初回wire/framingも認証済みgrantまたはhost選択のより狭い上限内で実測し、その加算資源を子操作の上限から先に差し引く。受信したLimits自体を実行許可にしない。

HeadDelivery.usageの採取点は最終返信エンコードの直前で、framingとその時点までの子操作を含む。エンコード自身の費用を同じcounterへ再帰的に埋め込まない。host transportが観測・認証したエンコード後の全使用量を発行上限と照合して一度だけsettleし、Work・Allocation等を親へ記録する。親が既に停止していても観測済み子実費は記録し、元の停止理由を保持する。子の終了と観測量が確定したら不正返信のデコードより先に精算し、後続の非停止拒否でも元の待機要求を再試行できるようにする。精算後は未使用の貸出分のみを親へ戻し、accept時の返信検査もその親Budgetで計上する。未精算proofの破棄は親をCancelledにして、まだ動作し得る子への貸出を再利用しない。窓SourceBytesだけは保存発行proofにより再加算せず、Depthはmaxで合流する。Report.usageは発行基準から返信採取点の累積値へ変換する。独立processの通信認証・停止制御・メータリング方式はhost実装の責務であり、NDF型検査や受信自己申告だけではその証拠を発行しない。子が最終エンコード前に停止した場合も、hostは確定した実観測量を精算できるが、停止Budgetから成功packetを作れるとはしない。

現在のParseTree.validateは静的選択・参照所有・回復構文・payload型に加え、Dynamicのalias/categoryに登録された実provider、操作署名、固定shape、各child contextとの整合を検査する。既知の静的formに一致するheadをDynamicとして受理しない。未登録providerや整合しない選択は拒否する。この検査はcallbackの実行履歴を認証せず、任意のreader/providerを再実行して全payloadがその出力であることを証明するものでもない。nativeの動的選択実行、portable構造の往復、provider初回受信と返信照合はそれぞれ実行試験で区別し、全体のP03完成を単独のtree検査から推定しない。

Unparsedの先頭をtokenとして既に読んでいる場合は、そのTokenRefとheadを保持し、Unparsed coverがheadを包含することを検査する。未知arityを推測して通常leafへ変えることと、既読tokenのpayload/view/triviaを保存することは別である。tokenを得られないNoMatch等ではtoken/headをともにNoneとする。どちらの場合も不明範囲と理由はRecoveryEntryに残る。

8. Grammar自身のbootstrap

検査済みParseTreeは、同じ不変なSyntaxBundleに対して成立したsource・型・参照の検査proofを借用で公開できる。RustのValidatedParseTree::syntaxvalidate_with_sourcesの結果を保持して返し、同じ操作内でのlower準備に再検査・再計上を要求しない。raw入力、変更したtree、別のsnapshotへこのproofを付け替えてはならない。環境内容digestの一致やDSLの意味検査まで証明したものとは扱わず、それらの検査は引き続き必要である。proofを使う下流操作自身の処理量とsource admissionは省略しない。

完全な文法表からseed descriptorを生成し、通常engineで自分のlanguage定義を読む。seedのarity手書き表とsourceを独立に二重管理しない。生成した全表・source・seedの対応を機械検査する。

Grammar packageの利用者が機能を拡張しても共通engineを書き換えない。編集対象の文法を変更したら依存package/queryを無効化し、schema digestの異なる結果を混用しない。

WithMode の所属と復帰

withmode M R は R の構文rootを所有するpackageのmode Mを選ぶ。Builtin・Local・ListOfのrootは現在packageに属し、Foreignのrootはaliasが指すguestに属する。入れ子のWithModeは内側のrootまで所属をたどり、同じrootに複数overrideがある場合は最内側を使う。無効な外側mode宣言も黙殺せず、対応ownerのmodeとして検査する。

withmode Code (listof (foreign Guest Sentence)) はhostのcons/nil spineをCodeで読み、各guest要素はSentenceの既定modeを使う。listof (withmode GuestCode (foreign Guest Sentence)) はhost listの既定modeを保ち、guest要素のrootだけGuestCodeを使う。hostの同名modeはguest modeの代用にならない。Builtinは選択modeのskipを使い、値のreaderは指定builtinを直接使う。

overrideはそのrootへ適用する。通常formの各childは自身のReadSpecで新しいcontextを選び、親のoverrideを暗黙継承しない。同じlistのtailはspine modeを継続する。foreign終了時は保存したhost contextへ戻る。実prefix試験ではhostとguestに同名で異なるreaderのmodeを置き、所属・list tail・child・復帰を検査する。

現在のLanguagePackage::checkは局所metadataとshapeの検査であり、Foreignのalias/category/modeは解決済Profileで検査する対象として残る。package意味digest、解決済EntryContext/Profile、実parse/Grammar bootstrapをこの局所proofから推定しない。

現在の正本: Markdown原文。NEPL3dへの移行は別途進めています。