Add associative map constraints and range refinement

doc/manual/souce/design/execution-pipeline.md

@@ -16,7 +16,8 @@ demand-driven evaluation
   ├─ load imported module on demand
   ├─ evaluate expression
   ├─ compose `&`
-  └─ patch `//`
+  ├─ patch `//`
+  └─ validate `as`
   ↓
 materialize
   ↓
@@ -105,9 +106,16 @@ eval(A // B):
   a = eval(A)
   b = eval(B)
   patch(a, b)
+
+eval(A as S):
+  narrower = eval(A)
+  wider = eval(S)
+  apply_as(narrower, wider)
 ```
 
-`&` は制約を保った合成を行い、`//` は右辺優先の deep patch を行う。
+`&` は制約を保った対称な合成を行い、`//` は右辺優先の deep patch を行う。
+`as` は左辺が右辺より狭いことを再帰的に確認する。左辺で絞られた部分は左辺を使い、右辺だけの部分は abstract のまま保持する。
+default は `as` では選択せず、materialize まで遅延する。
 詳細は [Composition and Materialization](./composition-and-materialization.md) に置く。
 
 ## resolver / binder
@@ -140,7 +148,7 @@ resolver / binder を追加すると、以下を早期に診断しやすくな
 - import path の一部静的解決
 - span 付き diagnostic の精度向上
 
-ただし、Decodal の制約検証は独立した type checking pass ではなく、`&` の合成時や materialize 時に行う。
+ただし、Decodal の制約検証は独立した type checking pass ではなく、`&` の合成時、`as` の適用時、materialize 時に行う。
 
 ## materialize