@@ -774,38 +774,39 @@
774:: (face 2:11 items
774:: (face 2:11 items
775:: (apply 2:17 list (aura 2:23 @t)))
775:: (apply 2:17 list (aura 2:23 @t)))
776:: (face 2:27 open (flag 2:32))))
776:: (face 2:27 open (flag 2:32))))
777−:: (mold 3:1 poke
777+:: (mold 3:1 cart-action
778:: (union 4:3
778:: (union 4:3
779:: (cell 4:3
779:: (cell 4:3
780:: (const 4:4 %add)
780:: (const 4:4 %add)
781:: (face 4:9 item (aura 4:14 @t)))
781:: (face 4:9 item (aura 4:14 @t)))
782:: (const 5:3 %toggle)))
782:: (const 5:3 %toggle)))
783+:: (mold 6:1 poke (ref 6:9 cart-action))
783−:: (value 7:1 main
784+:: (value 8:1 main
784−:: (group 7:9
785+:: (group 8:9
785−:: (call 7:10 (wing 7:10 store) (wing 7:16 init) (wing 7:21 update))))
786+:: (call 8:10 (wing 8:10 store) (wing 8:16 init) (wing 8:21 update))))
786−:: (value 8:1 init
787+:: (value 9:1 init
787−:: (cast 8:9
788+:: (cast 9:9
788−:: (ref 8:12 state)
789+:: (ref 9:12 state)
789−:: (tuple 8:18 (lit 8:19 ~) (lit 8:21 %.n))))
790+:: (tuple 9:18 (lit 9:19 ~) (lit 9:21 %.n))))
790−:: (value 9:1 update
791+:: (value 10:1 update
791−:: (gate 9:11
792+:: (gate 10:11
792−:: (cell 9:14
793+:: (cell 10:14
793−:: (face 9:15 a (ref 9:17 poke))
794+:: (face 10:15 a (ref 10:17 cart-action))
794−:: (face 9:22 s (ref 9:24 state)))
795+:: (face 10:29 s (ref 10:31 state)))
795−:: (body 10:3
796+:: (body 11:3
796−:: (branch 10:3
797+:: (branch 11:3
797−:: (wing 10:6 a)
798+:: (wing 11:6 a)
799−:: (cell 11:5 (lit 11:6 %add) (bind 11:11 item))
802−:: (tuple 11:26 (wing 11:27 item) (wing 11:32 items.s)))))
803:: (arm 12:5
799:: (arm 12:5
804−:: (lit 12:5 %toggle)
800+:: (cell 12:5 (lit 12:6 %add) (bind 12:11 item))
805:: (change 12:18 s
801:: (change 12:18 s
806−:: (edit 12:20 open
802+:: (edit 12:20 items
803+:: (tuple 12:26 (wing 12:27 item) (wing 12:32 items.s)))))
805+:: (lit 13:5 %toggle)
807−:: (group 12:25
808+:: (group 13:25
808−:: (call 12:26 (wing 12:26 not) (wing 12:30 open.s)))))))))))
809+:: (call 13:26 (wing 13:26 not) (wing 13:30 open.s)))))))))))
810:: 4.3 Errors (+show-error): "<file>:<line>:<col>: <message>", then the
811:: 4.3 Errors (+show-error): "<file>:<line>:<col>: <message>", then the
811:: source line, then a caret under the column (col - 1 spaces, then ^).
812:: source line, then a caret under the column (col - 1 spaces, then ^).
@@ -1633,14 +1634,9 @@
1634:: +bad-char: the error for a character that no text may hold (2.2)
1635:: +bad-char: the error for a character that no text may hold (2.2)
1636−:: The line feed ends a line and is no such character, so an escape
1637−:: cut off by the end of its line gets the same error as one cut off
1638−:: by the end of the text.
1640++ bad-char
1637++ bad-char
1642 ^- (unit tape)
1639 ^- (unit tape)
1644 ?: =(9 c) `"a tab: Jibb uses spaces only"
1640 ?: =(9 c) `"a tab: Jibb uses spaces only"
1645 ?: =(13 c) `"a carriage return: Jibb lines end with a line feed alone"
1641 ?: =(13 c) `"a carriage return: Jibb lines end with a line feed alone"
1646 ?: |((lth c 32) =(127 c)) `"a control character"
1642 ?: |((lth c 32) =(127 c)) `"a control character"
@@ -4662,8 +4658,7 @@
4664 $~ [%var 0]
4660 $~ [%var 0]
4665− $% [%var id=@ud]
4661+ $% [%var id=@ud]
4667 [%avar id=@ud]
4662 [%avar id=@ud]
4668 [%rvar id=@ud]
4663 [%rvar id=@ud]
4669 [%nvar id=@ud]
4664 [%nvar id=@ud]
@@ -4686,7 +4681,7 @@
4687+$ ibinding [id=@ud val=itype]
4682+$ ibinding [id=@ud val=itype]
4688+$ isub (list ibinding)
4683+$ isub (list ibinding)
4689−+$ ipending [id=@ud literal=lit at=span]
4684++$ ipending [id=@ud literal=lit]
4691++ itype-lookup
4686++ itype-lookup
4692 |= [n=@ud sub=isub]
4687 |= [n=@ud sub=isub]
@@ -4699,35 +4694,35 @@
4699 |= [t=itype sub=isub]
4694 |= [t=itype sub=isub]
4700 ^- itype
4695 ^- itype
4701 ?+ -.t t
4696 ?+ -.t t
4702− ?(%var %fvar)
4697+ %var
4703 =/ found=(unit itype) (itype-lookup id.t sub)
4698 =/ found=(unit itype) (itype-lookup id.t sub)
4704 ?~ found t
4699 ?~ found t
4705− ?: &(|(?=(%fvar -.u.found) ?=(%rvar -.u.found) ?=(%rnvar -.u.found)) =(id.t +.u.found)) u.found
4700+ ?: &(|(?=(%rvar -.u.found) ?=(%rnvar -.u.found)) =(id.t +.u.found)) u.found
4706 $(t u.found)
4701 $(t u.found)
4708 =/ found=(unit itype) (itype-lookup id.t sub)
4703 =/ found=(unit itype) (itype-lookup id.t sub)
4709 ?~ found t
4704 ?~ found t
4710− ?: &(|(?=(%fvar -.u.found) ?=(%rvar -.u.found) ?=(%rnvar -.u.found)) =(id.t +.u.found)) u.found
4705+ ?: &(|(?=(%rvar -.u.found) ?=(%rnvar -.u.found)) =(id.t +.u.found)) u.found
4711 $(t u.found)
4706 $(t u.found)
4713 =/ found=(unit itype) (itype-lookup id.t sub)
4708 =/ found=(unit itype) (itype-lookup id.t sub)
4714 ?~ found t
4709 ?~ found t
4715− ?: &(|(?=(%fvar -.u.found) ?=(%rvar -.u.found) ?=(%rnvar -.u.found)) =(id.t +.u.found)) u.found
4710+ ?: &(|(?=(%rvar -.u.found) ?=(%rnvar -.u.found)) =(id.t +.u.found)) u.found
4716 $(t u.found)
4711 $(t u.found)
4718 =/ found=(unit itype) (itype-lookup id.t sub)
4713 =/ found=(unit itype) (itype-lookup id.t sub)
4719 ?~ found t
4714 ?~ found t
4720− ?: &(|(?=(%fvar -.u.found) ?=(%rvar -.u.found) ?=(%rnvar -.u.found)) =(id.t +.u.found)) u.found
4715+ ?: &(|(?=(%rvar -.u.found) ?=(%rnvar -.u.found)) =(id.t +.u.found)) u.found
4721 $(t u.found)
4716 $(t u.found)
4723 =/ found=(unit itype) (itype-lookup id.t sub)
4718 =/ found=(unit itype) (itype-lookup id.t sub)
4724 ?~ found t
4719 ?~ found t
4725− ?: &(|(?=(%fvar -.u.found) ?=(%rvar -.u.found) ?=(%rnvar -.u.found)) =(id.t +.u.found)) u.found
4720+ ?: &(|(?=(%rvar -.u.found) ?=(%rnvar -.u.found)) =(id.t +.u.found)) u.found
4726 $(t u.found)
4721 $(t u.found)
4728 =/ found=(unit itype) (itype-lookup id.t sub)
4723 =/ found=(unit itype) (itype-lookup id.t sub)
4729 ?~ found t
4724 ?~ found t
4730− ?: &(|(?=(%fvar -.u.found) ?=(%rvar -.u.found) ?=(%rnvar -.u.found)) =(id.t +.u.found)) u.found
4725+ ?: &(|(?=(%rvar -.u.found) ?=(%rnvar -.u.found)) =(id.t +.u.found)) u.found
4731 $(t u.found)
4726 $(t u.found)
@@ -4780,7 +4775,6 @@
4780 ?- -.typ
4775 ?- -.typ
4781 %empty `[%no fuel]
4776 %empty `[%no fuel]
4782 ?(%atom %any-atom %flag %const %noun %avar %rvar %nvar %rnvar %fn %jrec) `[%yes fuel]
4777 ?(%atom %any-atom %flag %const %noun %avar %rvar %nvar %rnvar %fn %jrec) `[%yes fuel]
4783− %fvar `[%unknown fuel]
4785 ?: (lien caps |=(c=icap (hole-same-variable typ (itype-walk [%var id.c] sub)))) `[%yes fuel]
4779 ?: (lien caps |=(c=icap (hole-same-variable typ (itype-walk [%var id.c] sub)))) `[%yes fuel]
4786 `[%unknown fuel]
4780 `[%unknown fuel]
@@ -4820,7 +4814,6 @@
4820 =. t (itype-walk t sub)
4814 =. t (itype-walk t sub)
4822 %var =(n id.t)
4816 %var =(n id.t)
4824 %avar =(n id.t)
4817 %avar =(n id.t)
4825 %rvar =(n id.t)
4818 %rvar =(n id.t)
4826 %nvar =(n id.t)
4819 %nvar =(n id.t)
@@ -4875,12 +4868,6 @@
4875 ?: ?=(%var -.b)
4868 ?: ?=(%var -.b)
4876 ?: (itype-occurs id.b a sub) ~
4869 ?: (itype-occurs id.b a sub) ~
4877 `[[id.b a] sub]
4870 `[[id.b a] sub]
4879− ?: (itype-occurs id.a b sub) ~
4880− (itype-bind-gate-free id.a b sub)
4882− ?: (itype-occurs id.b a sub) ~
4883− (itype-bind-gate-free id.b a sub)
4884 :: Arithmetic's aura variable excludes loobeans; decimal literals
4871 :: Arithmetic's aura variable excludes loobeans; decimal literals
4885 :: remain defaultable until a later constraint makes them concrete.
4872 :: remain defaultable until a later constraint makes them concrete.
4886 ?: &(?=(%nvar -.a) ?=(%rvar -.b))
4873 ?: &(?=(%nvar -.a) ?=(%rvar -.b))
@@ -4939,69 +4926,6 @@
4939 $(a tal.a, b tal.b, sub u.first)
4926 $(a tal.a, b tal.b, sub u.first)
4942−+$ igf-form [typ=itype sub=isub left=@ud]
4943−+$ igf-forms [types=(list itype) sub=isub left=@ud]
4944−++ itype-gate-free-forms
4945− |= [xs=(list itype) sub=isub fuel=@ud]
4946− ^- (unit igf-forms)
4947− ?~ xs `[~ sub fuel]
4948− =/ head=(unit igf-form) (itype-gate-free-form i.xs sub fuel)
4950− =/ tail=(unit igf-forms) $(xs t.xs, sub sub.u.head, fuel left.u.head)
4952− `[[typ.u.head types.u.tail] sub.u.tail left.u.tail]
4954−++ itype-gate-free-form
4955− |= [t=itype sub=isub fuel=@ud]
4959− =. t (itype-walk t sub)
4962− =/ free=itype [%fvar id.t]
4963− `[free [[id.t free] sub] fuel]
4964− %fvar `[t sub fuel]
4965− ?(%atom %any-atom %flag %const %empty %avar %rvar %nvar %rnvar %jrec) `[t sub fuel]
4967− =/ body=(unit igf-form) $(t body.t, sub sub, fuel fuel)
4969− `[[%face name.t typ.u.body] sub.u.body left.u.body]
4971− =/ head=(unit igf-form) $(t hed.t, sub sub, fuel fuel)
4973− =/ tail=(unit igf-form) $(t tal.t, sub sub.u.head, fuel left.u.head)
4975− `[[%cell typ.u.head typ.u.tail] sub.u.tail left.u.tail]
4977− =/ args=(unit igf-forms) (itype-gate-free-forms args.t sub fuel)
4979− `[[%collection name.t types.u.args] sub.u.args left.u.args]
4981− =/ cases=(unit igf-forms) (itype-gate-free-forms cases.t sub fuel)
4983− =/ args=(unit igf-forms) (itype-gate-free-forms args.t sub.u.cases left.u.cases)
4985− `[[%union types.u.cases origin.t label.t types.u.args] sub.u.args left.u.args]
4989−++ itype-collection-keys
4990− |= [name=term args=(list itype) sub=isub]
4991− ^- (unit [types=(list itype) sub=isub])
4993− ?. |(?=(?(%set %map %mop %jar %jug) name)) `[args sub]
4994− =/ key=(unit igf-form) (itype-gate-free-form i.args sub 256)
4996− `[[typ.u.key t.args] sub.u.key]
4998−++ itype-bind-gate-free
4999− |= [n=@ud t=itype sub=isub]
5001− =/ constrained=(unit igf-form) (itype-gate-free-form t sub 256)
5003− `[[n typ.u.constrained] sub.u.constrained]
5005++ itype-unify-args
4929++ itype-unify-args
5006 |= [as=(list itype) bs=(list itype) sub=isub]
4930 |= [as=(list itype) bs=(list itype) sub=isub]
5007 ^- (unit isub)
4931 ^- (unit isub)
@@ -5023,11 +4947,10 @@
5023 =. t (itype-walk t sub)
4947 =. t (itype-walk t sub)
5030− %rnvar |
4953+ %rnvar |
5032 %any-atom &
4955 %any-atom &
@@ -5100,7 +5023,6 @@
5101 ?- -.typ
5024 ?- -.typ
@@ -5208,8 +5130,8 @@
5208 ?. =(name.a name.b) |
5130 ?. =(name.a name.b) |
5209 (itype-face-asym-collection-args args.a args.b sub)
5131 (itype-face-asym-collection-args args.a args.b sub)
5210 ?: &(?=(%face -.a) ?=(%face -.b)) $(a body.a, b body.b)
5132 ?: &(?=(%face -.a) ?=(%face -.b)) $(a body.a, b body.b)
5211− ?: ?=(%face -.a) !|(?=(%var -.b) ?=(%fvar -.b) ?=(%avar -.b) ?=(%rvar -.b) |(?=(%nvar -.b) ?=(%rnvar -.b)))
5133+ ?: ?=(%face -.a) !|(?=(%var -.b) ?=(%avar -.b) ?=(%rvar -.b) |(?=(%nvar -.b) ?=(%rnvar -.b)))
5212− ?: ?=(%face -.b) !|(?=(%var -.a) ?=(%fvar -.a) ?=(%avar -.a) ?=(%rvar -.a) |(?=(%nvar -.a) ?=(%rnvar -.a)))
5134+ ?: ?=(%face -.b) !|(?=(%var -.a) ?=(%avar -.a) ?=(%rvar -.a) |(?=(%nvar -.a) ?=(%rnvar -.a)))
5213 ?: &(?=(%cell -.a) ?=(%cell -.b)) |($(a hed.a, b hed.b) $(a tal.a, b tal.b))
5135 ?: &(?=(%cell -.a) ?=(%cell -.b)) |($(a hed.a, b hed.b) $(a tal.a, b tal.b))
5214 ?: &(?=(%fn -.a) ?=(%fn -.b)) |($(a sample.a, b sample.b) $(a product.a, b product.b))
5136 ?: &(?=(%fn -.a) ?=(%fn -.b)) |($(a sample.a, b sample.b) $(a product.a, b product.b))
@@ -5281,13 +5203,6 @@
5281 ?~ (itype-lookup id.i.tags sub) &
5203 ?~ (itype-lookup id.i.tags sub) &
5282 $(tags t.tags)
5204 $(tags t.tags)
5284−++ pending-tag-diagnostic
5285− |= [tags=(list ipending) sub=isub]
5286− ^- (unit [at=span msg=tape])
5288− ?^ (itype-lookup id.i.tags sub) $(tags t.tags)
5289− `[at.i.tags (weld "nothing fixes the union of " (show-lit literal.i.tags))]
5291++ pending-null
5206++ pending-null
5292 |= [tags=(list ipending) sub=isub]
5207 |= [tags=(list ipending) sub=isub]
@@ -5462,9 +5377,9 @@
5462 ?: too-wide [%unknown ~]
5377 ?: too-wide [%unknown ~]
5463 =/ spine-checked=? |(spine-proof ?=(^ known))
5378 =/ spine-checked=? |(spine-proof ?=(^ known))
5464 =/ uncertain=?
5379 =/ uncertain=?
5465− |(?=(%var -.actual) ?=(%fvar -.actual) ?=(%avar -.actual) ?=(%rvar -.actual) |(?=(%nvar -.actual) ?=(%rnvar -.actual)) ?=(%var -.expected) ?=(%fvar -.expected) ?=(%avar -.expected) ?=(%rvar -.expected) |(?=(%nvar -.expected) ?=(%rnvar -.expected)))
5380+ |(?=(%var -.actual) ?=(%avar -.actual) ?=(%rvar -.actual) |(?=(%nvar -.actual) ?=(%rnvar -.actual)) ?=(%var -.expected) ?=(%avar -.expected) ?=(%rvar -.expected) |(?=(%nvar -.expected) ?=(%rnvar -.expected)))
5466 =/ actual-open=?
5381 =/ actual-open=?
5467− |(?=(%var -.actual) ?=(%fvar -.actual) ?=(%avar -.actual) ?=(%rvar -.actual) |(?=(%nvar -.actual) ?=(%rnvar -.actual)))
5382+ |(?=(%var -.actual) ?=(%avar -.actual) ?=(%rvar -.actual) |(?=(%nvar -.actual) ?=(%rnvar -.actual)))
5468 =. actual (itype-walk actual sub)
5383 =. actual (itype-walk actual sub)
5469 =. expected (itype-walk expected sub)
5384 =. expected (itype-walk expected sub)
5470 ?: =(actual expected) [%ok sub next]
5385 ?: =(actual expected) [%ok sub next]
@@ -5519,7 +5434,7 @@
5519 ?: &(!uncertain ?=(%union -.actual) ?=(%face -.expected))
5434 ?: &(!uncertain ?=(%union -.actual) ?=(%face -.expected))
5520 $(expected body.expected)
5435 $(expected body.expected)
5521 ?: ?=(%union -.actual) [%unknown ~]
5436 ?: ?=(%union -.actual) [%unknown ~]
5522− ?: &(?=(%union -.expected) |(?=(%fvar -.actual) ?=(%avar -.actual) ?=(%rvar -.actual) |(?=(%nvar -.actual) ?=(%rnvar -.actual)))) [%unknown ~]
5437+ ?: &(?=(%union -.expected) |(?=(%avar -.actual) ?=(%rvar -.actual) |(?=(%nvar -.actual) ?=(%rnvar -.actual)))) [%unknown ~]
5523 ?: &(?=(%union -.expected) !?=(%var -.actual))
5438 ?: &(?=(%union -.expected) !?=(%var -.actual))
5524 (itype-fit-cases actual cases.expected sub next)
5439 (itype-fit-cases actual cases.expected sub next)
5525 ?: ?=(%tag -.actual)
5440 ?: ?=(%tag -.actual)
@@ -5527,7 +5442,7 @@
5527 =/ u=(unit isub) (itype-unify actual expected sub)
5442 =/ u=(unit isub) (itype-unify actual expected sub)
5528 ?~ u [%bad ~]
5443 ?~ u [%bad ~]
5529 [%ok u.u next]
5444 [%ok u.u next]
5530− ?: |(?=(%fvar -.expected) ?=(%avar -.expected) ?=(%rvar -.expected) |(?=(%nvar -.expected) ?=(%rnvar -.expected))) [%unknown ~]
5445+ ?: |(?=(%avar -.expected) ?=(%rvar -.expected) |(?=(%nvar -.expected) ?=(%rnvar -.expected))) [%unknown ~]
5531 ?: ?=(%face -.expected) $(expected body.expected)
5446 ?: ?=(%face -.expected) $(expected body.expected)
5532 ?: constructor.actual
5447 ?: constructor.actual
5533 ?. ?=(%fn -.expected) [%bad ~]
5448 ?. ?=(%fn -.expected) [%bad ~]
@@ -5555,7 +5470,7 @@
5555 =/ u=(unit isub) (itype-unify actual expected sub)
5470 =/ u=(unit isub) (itype-unify actual expected sub)
5556 ?~ u [%bad ~]
5471 ?~ u [%bad ~]
5557 [%ok u.u next]
5472 [%ok u.u next]
5558− ?: |(?=(%fvar -.expected) ?=(%avar -.expected) ?=(%rvar -.expected) |(?=(%nvar -.expected) ?=(%rnvar -.expected))) [%unknown ~]
5473+ ?: |(?=(%avar -.expected) ?=(%rvar -.expected) |(?=(%nvar -.expected) ?=(%rnvar -.expected))) [%unknown ~]
5559 ?: ?=(%face -.expected) $(expected body.expected)
5474 ?: ?=(%face -.expected) $(expected body.expected)
5560 ?: &(?=(%collection -.expected) =(%list name.expected) =(0 val.literal.actual))
5475 ?: &(?=(%collection -.expected) =(%list name.expected) =(0 val.literal.actual))
5561 [%unknown ~]
5476 [%unknown ~]
@@ -5572,13 +5487,6 @@
5572 ?:(|(=(0 val.literal.actual) =(1 val.literal.actual)) [%ok sub next] [%bad ~])
5487 ?:(|(=(0 val.literal.actual) =(1 val.literal.actual)) [%ok sub next] [%bad ~])
5573 ?: ?=(%any-atom -.expected) [%ok sub next]
5488 ?: ?=(%any-atom -.expected) [%ok sub next]
5574 [%bad ~]
5489 [%bad ~]
5575− :: A field on an expected sample slot labels the value's type; it does
5576− :: not become a face on the actual argument. Unify with the slot body
5577− :: rather than binding either variable to the face around the other.
5578− ?: &(?=(%var -.actual) ?=(%face -.expected))
5579− =/ unified=(unit isub) (itype-unify actual body.expected sub)
5580− ?~ unified [%unknown ~]
5581− [%ok u.unified next]
5582 ?: &(uncertain (itype-face-asym actual expected sub)) [%unknown ~]
5490 ?: &(uncertain (itype-face-asym actual expected sub)) [%unknown ~]
5583 :: A known face labels the same noun. Peel it before applying the
5491 :: A known face labels the same noun. Peel it before applying the
5584 :: directional unrestricted-atom rule, preserving raw-variable guards.
5492 :: directional unrestricted-atom rule, preserving raw-variable guards.
@@ -5598,7 +5506,7 @@
5598 =/ unified=(unit isub) (itype-unify actual expected sub)
5506 =/ unified=(unit isub) (itype-unify actual expected sub)
5599 ?~ unified [%bad ~]
5507 ?~ unified [%bad ~]
5600 [%ok u.unified next]
5508 [%ok u.unified next]
5601− ?: |(?=(%fvar -.expected) ?=(%avar -.expected) ?=(%rvar -.expected) |(?=(%nvar -.expected) ?=(%rnvar -.expected))) [%unknown ~]
5509+ ?: |(?=(%avar -.expected) ?=(%rvar -.expected) |(?=(%nvar -.expected) ?=(%rnvar -.expected))) [%unknown ~]
5602 [%bad ~]
5510 [%bad ~]
5603 ?: &(?=(%atom -.actual) ?=(%atom -.expected))
5511 ?: &(?=(%atom -.actual) ?=(%atom -.expected))
5604 ?: (aura-prefix aura.expected aura.actual) [%ok sub next]
5512 ?: (aura-prefix aura.expected aura.actual) [%ok sub next]
@@ -5608,10 +5516,18 @@
5608 =/ first=ifit $(actual hed.actual, expected hed.expected, skip-width |, spine-proof |)
5516 =/ first=ifit $(actual hed.actual, expected hed.expected, skip-width |, spine-proof |)
5609 ?. ?=(%ok -.first) first
5517 ?. ?=(%ok -.first) first
5610 $(actual tal.actual, expected tal.expected, sub sub.first, next next.first, skip-width spine-checked, spine-proof spine-checked)
5518 $(actual tal.actual, expected tal.expected, sub sub.first, next next.first, skip-width spine-checked, spine-proof spine-checked)
5519+ :: A field may add a face to an occurrence of the very same type
5520+ :: variable. Binding that variable to a face around itself would fail
5521+ :: the occurs check, but its underlying type has already matched.
5522+ ?: &(?=(%var -.actual) ?=(%face -.expected) =(actual (itype-walk body.expected sub)))
5524+ :: Differing variables and faces need propagation that is not yet
5525+ :: represented. Binding one to the face can create a false mismatch.
5526+ ?: &(?=(%var -.actual) ?=(%face -.expected)) [%unknown ~]
5611 ?: &(?=(%face -.actual) ?=(%var -.expected)) [%unknown ~]
5527 ?: &(?=(%face -.actual) ?=(%var -.expected)) [%unknown ~]
5612 ?: &(?=(%var -.actual) (itype-has-any-atom expected sub))
5528 ?: &(?=(%var -.actual) (itype-has-any-atom expected sub))
5613 [%unknown ~]
5529 [%unknown ~]
5614− ?: |(?=(%var -.actual) ?=(%var -.expected) ?=(%fvar -.expected))
5530+ ?: |(?=(%var -.actual) ?=(%var -.expected))
5615 =/ unified=(unit isub) (itype-unify actual expected sub)
5531 =/ unified=(unit isub) (itype-unify actual expected sub)
5616 ?~ unified
5532 ?~ unified
5617 ?: |(?=(%face -.actual) ?=(%face -.expected)) [%unknown ~]
5533 ?: |(?=(%face -.actual) ?=(%face -.expected)) [%unknown ~]
@@ -5691,36 +5607,6 @@
5691 (itype-fit [%collection %list ~[a]] list-t ~[[0 recursive]] 1)
5607 (itype-fit [%collection %list ~[a]] list-t ~[[0 recursive]] 1)
5692 =? problems !?=(%unknown -.nested-fit)
5608 =? problems !?=(%unknown -.nested-fit)
5693 ["recursive types behind substitutions should remain uncertain" problems]
5609 ["recursive types behind substitutions should remain uncertain" problems]
5694− =/ free=itype [%fvar 40]
5695− =/ open-cell=itype [%cell [%var 41] [%face %x [%var 42]]]
5696− =/ constrained=(unit isub) (itype-unify free open-cell ~)
5697− =/ expected-cell=itype [%cell [%fvar 41] [%face %x [%fvar 42]]]
5698− =? problems !=(constrained [~ [[40 expected-cell] [[42 [%fvar 42]] [[41 [%fvar 41]] ~]]]])
5699− ["gate-free constraints should propagate through cells and faces" problems]
5700− =? problems ?=(^ (itype-unify free open-cell ~[[41 [%fn txt txt]]]))
5701− ["an existing nested gate substitution should be rejected" problems]
5702− =/ shared-sub=isub [[42 [%fvar 42]] [[41 [%fvar 41]] ~]]
5703− =? problems ?=(^ (itype-unify [%var 41] [%fn txt txt] shared-sub))
5704− ["a later nested gate substitution should be rejected" problems]
5705− =? problems ?=(^ (itype-unify free [%fn txt txt] ~))
5706− ["a gate-free variable should reject a gate" problems]
5707− =? problems ?=(^ (itype-unify free [%noun ~] ~))
5708− ["a gate-free variable should reject an opaque noun" problems]
5709− =/ atom-strong=(unit isub) (itype-unify [%avar 43] free ~)
5710− =? problems !=(atom-strong [~ [[40 [%avar 43]] ~]])
5711− ["the atom constraint should be stronger than gate-free" problems]
5712− =/ free-fit=ifit (itype-fit txt free ~ 44)
5713− =? problems !?=(%ok -.free-fit)
5714− ["a concrete atom should fit a gate-free variable" problems]
5715− =/ gate-fit=ifit (itype-fit [%fn txt txt] free ~ 44)
5716− =? problems !?=(%bad -.gate-fit)
5717− ["a gate should not fit a gate-free variable" problems]
5718− =/ free-scheme=ischeme [[%fn free free] ~[40]]
5719− =/ canonical-free=itype (canonical-itype typ.free-scheme vars.free-scheme)
5720− =? problems !=(canonical-free [%fn [%fvar 0] [%fvar 0]])
5721− ["canonicalization should retain gate-free variables" problems]
5722− =? problems !=((show-atom-constraint canonical-free) " where A contains no gates")
5723− ["the printer should show gate-free constraints" problems]
5724 problems
5610 problems
5726:: The expression inference below is deliberately a fragment: bindings,
5612:: The expression inference below is deliberately a fragment: bindings,
@@ -5737,14 +5623,10 @@
5737:: of an arbitrary ask value. Reader graphs and source inputs are trusted.
5623:: of an arbitrary ask value. Reader graphs and source inputs are trusted.
5738+$ irequest-evidence
5624+$ irequest-evidence
5739 [api-at=path name=term path=iapi-path-typed api-source=@t public-source=@t internal-source=@t prelude-values=(list term) prelude-molds=(list term) externals=iexternals marks=imark-externals]
5625 [api-at=path name=term path=iapi-path-typed api-source=@t public-source=@t internal-source=@t prelude-values=(list term) prelude-molds=(list term) externals=iexternals marks=imark-externals]
5740−:: Store requests have their own source-bound evidence. In particular, an
5741−:: API path certificate cannot make a store state member watchable, or vice versa.
5742−+$ istore-request-evidence
5743− [store-at=path source=@t state=itype action-name=term action=itype]
5744:: A unit distinguishes a verified empty closure from a detached legacy file.
5626:: A unit distinguishes a verified empty closure from a detached legacy file.
5745:: The opaque prelude is an exact trusted input, not a recursive interface mold.
5627:: The opaque prelude is an exact trusted input, not a recursive interface mold.
5746+$ irequest-graph
5628+$ irequest-graph
5747− [paths=(set path) requests=(list irequest-evidence) stores=(list istore-request-evidence) bundle-input=* prelude-input=* prelude-values=(list term) prelude-molds=(list term) externals=iexternals marks=imark-externals]
5629+ [paths=(set path) requests=(list irequest-evidence) bundle-input=* prelude-input=* prelude-values=(list term) prelude-molds=(list term) externals=iexternals marks=imark-externals]
5748+$ ifile [values=ienv molds=imold-types at=path derived=(list iderived) elaborations=(list iwidth-definition) dependencies=(list iwidth-dependency) source=(unit @t) graph=(unit irequest-graph)]
5630+$ ifile [values=ienv molds=imold-types at=path derived=(list iderived) elaborations=(list iwidth-definition) dependencies=(list iwidth-dependency) source=(unit @t) graph=(unit irequest-graph)]
5749+$ ijimports (list [face=term interface=ifile])
5631+$ ijimports (list [face=term interface=ifile])
5750+$ icap [name=@t id=@ud at=span]
5632+$ icap [name=@t id=@ud at=span]
@@ -5906,7 +5788,6 @@
5906 %noun [%unknown & fuel ~]
5788 %noun [%unknown & fuel ~]
5907 %empty [%yes | fuel ~]
5789 %empty [%yes | fuel ~]
5908 %var [%unknown | fuel ~]
5790 %var [%unknown | fuel ~]
5909− %fvar [%yes & fuel ~]
5910 %avar [%yes & fuel ~]
5791 %avar [%yes & fuel ~]
5911 %rvar [%yes & fuel ~]
5792 %rvar [%yes & fuel ~]
5912 %nvar [%yes & fuel ~]
5793 %nvar [%yes & fuel ~]
@@ -5973,11 +5854,10 @@
5974 %const |
5855 %const |
5980− %rnvar |
5860+ %rnvar |
5982 %any-atom |
5862 %any-atom |
@@ -6008,7 +5888,6 @@
6008 ^- (unit @ud)
5888 ^- (unit @ud)
6010 %var `id.t
5890 %var `id.t
6012 %avar `id.t
5891 %avar `id.t
6013 %rvar `id.t
5892 %rvar `id.t
6014 %nvar `id.t
5893 %nvar `id.t
@@ -6029,7 +5908,7 @@
6030 =. t (itype-walk t sub.state)
5909 =. t (itype-walk t sub.state)
6032− ?(%var %fvar %avar %rvar %nvar %rnvar)
5911+ ?(%var %avar %rvar %nvar %rnvar)
6033 ?: (lien caps.state |=(c=icap (hole-same-variable t (itype-walk [%var id.c] sub.state)))) &
5912 ?: (lien caps.state |=(c=icap (hole-same-variable t (itype-walk [%var id.c] sub.state)))) &
6034 (lien params.state |=(p=[name=@t typ=itype] (hole-same-variable t (itype-walk typ.p sub.state))))
5913 (lien params.state |=(p=[name=@t typ=itype] (hole-same-variable t (itype-walk typ.p sub.state))))
@@ -6081,7 +5960,7 @@
6082 =. t (itype-walk t sub.state)
5961 =. t (itype-walk t sub.state)
6084− ?(%tag %nvar %rnvar %fvar %avar %rvar) !(hole-known t state)
5963+ ?(%tag %nvar %rnvar %avar %rvar) !(hole-known t state)
6085 %union |((lien cases.t |=(c=itype (hole-uncertain c state))) (lien args.t |=(c=itype (hole-uncertain c state))))
5964 %union |((lien cases.t |=(c=itype (hole-uncertain c state))) (lien args.t |=(c=itype (hole-uncertain c state))))
6086 %grec (lien args.t |=(c=itype (hole-uncertain c state)))
5965 %grec (lien args.t |=(c=itype (hole-uncertain c state)))
6087 %collection (lien args.t |=(c=itype (hole-uncertain c state)))
5966 %collection (lien args.t |=(c=itype (hole-uncertain c state)))
@@ -6099,19 +5978,14 @@
6099 ?~ work ~
5978 ?~ work ~
6100 ?: (hole-known [%var id.i.work] state) $(work t.work)
5979 ?: (hole-known [%var id.i.work] state) $(work t.work)
6101 ?: (hole-uncertain [%var id.i.work] state)
5980 ?: (hole-uncertain [%var id.i.work] state)
6102− `[uncertain-hole-msg ~[[at.i.work "type hole"]]]
5981+ `["type hole needs unsupported inference" ~[[at.i.work "type hole"]]]
6103 `["type hole needs a determined type" ~[[at.i.work "unresolved type hole"]]]
5982 `["type hole needs a determined type" ~[[at.i.work "unresolved type hole"]]]
6105−:: +uncertain-hole-msg: unsupported, though it names the hole's site
6107−++ uncertain-hole-msg "type hole needs unsupported inference"
6109++ itype-vars
5984++ itype-vars
6110 |= t=itype
5985 |= t=itype
6111 ^- (list @ud)
5986 ^- (list @ud)
6113 %var ~[id.t]
5988 %var ~[id.t]
6115 %avar ~[id.t]
5989 %avar ~[id.t]
6116 %rvar ~[id.t]
5990 %rvar ~[id.t]
6117 %nvar ~[id.t]
5991 %nvar ~[id.t]
@@ -6150,10 +6024,6 @@
6150 =/ found=(unit itype) (itype-lookup id.t ren)
6024 =/ found=(unit itype) (itype-lookup id.t ren)
6151 ?~ found t
6025 ?~ found t
6154− =/ found=(unit itype) (itype-lookup id.t ren)
6158 =/ found=(unit itype) (itype-lookup id.t ren)
6028 =/ found=(unit itype) (itype-lookup id.t ren)
6159 ?~ found t
6029 ?~ found t
@@ -6195,7 +6065,6 @@
6199 %avar =(n id.t)
6068 %avar =(n id.t)
6200 %rvar =(n id.t)
6069 %rvar =(n id.t)
6201 %nvar =(n id.t)
6070 %nvar =(n id.t)
@@ -6221,7 +6090,6 @@
6226 %rvar =(n id.t)
6094 %rvar =(n id.t)
@@ -6246,28 +6114,6 @@
6246:: Canonical numbering makes printed variables independent of the order
6114:: Canonical numbering makes printed variables independent of the order
6247:: the unifier happened to allocate intermediates.
6115:: the unifier happened to allocate intermediates.
6249−++ itype-var-is-gate-free-fuel
6250− |= [n=@ud t=itype fuel=@ud]
6257− %union |((lien cases.t |=(c=itype (itype-var-is-gate-free-fuel n c fuel))) (lien args.t |=(c=itype (itype-var-is-gate-free-fuel n c fuel))))
6258− %grec (lien args.t |=(c=itype (itype-var-is-gate-free-fuel n c fuel)))
6259− %collection (lien args.t |=(c=itype (itype-var-is-gate-free-fuel n c fuel)))
6260− %face $(t body.t, fuel fuel)
6261− %fn |($(t sample.t, fuel fuel) $(t product.t, fuel fuel))
6262− %cell |($(t hed.t, fuel fuel) $(t tal.t, fuel fuel))
6266−++ itype-var-is-gate-free
6269− (itype-var-is-gate-free-fuel n t 256)
6271++ canonical-itype
6117++ canonical-itype
6272 |= [t=itype vars=(list @ud)]
6118 |= [t=itype vars=(list @ud)]
6273 ^- itype
6119 ^- itype
@@ -6275,7 +6121,7 @@
6275 =/ n=@ud 0
6121 =/ n=@ud 0
6277 ?~ vars (itype-rename t ren)
6123 ?~ vars (itype-rename t ren)
6278− =/ replacement=itype ?:((itype-var-is-restricted i.vars t) [%rvar n] ?:((itype-var-is-atom i.vars t) [%avar n] ?:((itype-var-is-gate-free i.vars t) [%fvar n] [%var n])))
6124+ =/ replacement=itype ?:((itype-var-is-restricted i.vars t) [%rvar n] ?:((itype-var-is-atom i.vars t) [%avar n] [%var n]))
6279 $(vars t.vars, ren [[i.vars replacement] ren], n +(n))
6125 $(vars t.vars, ren [[i.vars replacement] ren], n +(n))
6281++ instantiate-scheme
6127++ instantiate-scheme
@@ -6286,11 +6132,11 @@
6287 ?~ vars [(itype-rename typ.scheme ren) state]
6133 ?~ vars [(itype-rename typ.scheme ren) state]
6288 =/ replacement=itype
6134 =/ replacement=itype
6289− ?:((itype-var-is-restricted i.vars typ.scheme) [%rvar next.state] ?:((itype-var-is-atom i.vars typ.scheme) [%avar next.state] ?:((itype-var-is-gate-free i.vars typ.scheme) [%fvar next.state] [%var next.state])))
6135+ ?:((itype-var-is-restricted i.vars typ.scheme) [%rvar next.state] ?:((itype-var-is-atom i.vars typ.scheme) [%avar next.state] [%var next.state]))
6290 :: A generalized atom variable is a valid origin for re-generalizing
6136 :: A generalized atom variable is a valid origin for re-generalizing
6291 :: an alias, just as a sample binder is.
6137 :: an alias, just as a sample binder is.
6292 =/ st=istate state(next +(next.state))
6138 =/ st=istate state(next +(next.state))
6293− =? binders.st |(?=(%fvar -.replacement) ?=(%avar -.replacement) ?=(%rvar -.replacement)) [next.state binders.state]
6139+ =? binders.st |(?=(%avar -.replacement) ?=(%rvar -.replacement)) [next.state binders.state]
6294 $(vars t.vars, ren [[i.vars replacement] ren], state st)
6140 $(vars t.vars, ren [[i.vars replacement] ren], state st)
6296++ icap-lookup
6142++ icap-lookup
@@ -6453,11 +6299,6 @@
6453++ import-to-itype
6299++ import-to-itype
6454 |= node=*
6300 |= node=*
6455 ^- (unit itype)
6301 ^- (unit itype)
6456− (import-to-itype-standard node ~)
6458−++ import-to-itype-standard
6459− |= [node=* standard=(unit ischeme)]
6461 ?@ node ~
6302 ?@ node ~
6462 ?+ -.node ~
6303 ?+ -.node ~
6463 %noun ?:(=(node [%noun ~]) `[%noun ~] ~)
6304 %noun ?:(=(node [%noun ~]) `[%noun ~] ~)
@@ -6499,24 +6340,16 @@
6499 ?: |(=(%map name) =(%mop name) =(%jar name) =(%jug name)) 2
6340 ?: |(=(%map name) =(%mop name) =(%jar name) =(%jug name)) 2
6501 ?: =(arity 0) ~
6342 ?: =(arity 0) ~
6502− =/ args=(unit (list itype)) (import-to-itypes-standard +>.node standard)
6343+ =/ args=(unit (list itype)) (import-to-itypes +>.node)
6503 ?~ args ~
6344 ?~ args ~
6504 ?. =(arity (lent u.args)) ~
6345 ?. =(arity (lent u.args)) ~
6505− =/ keyed=(unit [types=(list itype) sub=isub]) (itype-collection-keys name u.args ~)
6346+ `[%collection name u.args]
6508− ?. ?=([* ~] types.u.keyed) ~
6509− ?~ standard `[%collection name types.u.keyed]
6510− ?. (standard-unit-template u.standard /lib/jibb/prelude/jibb) ~
6511− =/ nil=itype [%const [%null %n 0 '~']]
6512− `[%union ~[nil [%cell nil [%face %u i.types.u.keyed]]] `[/lib/jibb/prelude/jibb %unit] `%unit types.u.keyed]
6513− `[%collection name types.u.keyed]
6515 :: Hoon's ordinary ? mold is the fork of its two %f singletons.
6348 :: Hoon's ordinary ? mold is the fork of its two %f singletons.
6516 =/ raw=* +.node
6349 =/ raw=* +.node
6517 ?: |(=(raw ~[[%atom %f `0] [%atom %f `1]]) =(raw ~[[%atom %f `1] [%atom %f `0]]))
6350 ?: |(=(raw ~[[%atom %f `0] [%atom %f `1]]) =(raw ~[[%atom %f `1] [%atom %f `0]]))
6518 `[%flag ~]
6351 `[%flag ~]
6519− =/ cases=(unit (list itype)) (import-to-itypes-standard raw standard)
6352+ =/ cases=(unit (list itype)) (import-to-itypes raw)
6520 ?~ cases ~
6353 ?~ cases ~
6521 ?~ u.cases ~
6354 ?~ u.cases ~
6522 ?~ t.u.cases ~
6355 ?~ t.u.cases ~
@@ -6556,15 +6389,10 @@
6556++ import-to-itypes
6389++ import-to-itypes
6557 |= nodes=*
6390 |= nodes=*
6558 ^- (unit (list itype))
6391 ^- (unit (list itype))
6559− (import-to-itypes-standard nodes ~)
6561−++ import-to-itypes-standard
6562− |= [nodes=* standard=(unit ischeme)]
6563− ^- (unit (list itype))
6564 ?@ nodes ?:(=(nodes 0) `~ ~)
6392 ?@ nodes ?:(=(nodes 0) `~ ~)
6565− =/ first (import-to-itype-standard -.nodes standard)
6393+ =/ first (import-to-itype -.nodes)
6566 ?~ first ~
6394 ?~ first ~
6567− =/ rest $(nodes +.nodes, standard standard)
6395+ =/ rest $(nodes +.nodes)
6568 ?~ rest ~
6396 ?~ rest ~
6569 `[u.first u.rest]
6397 `[u.first u.rest]
@@ -6591,10 +6419,9 @@
6591 ?. (levy t.cases |=(t=itype =(%disjoint (union-relate first (import-type-pattern t))))) |
6419 ?. (levy t.cases |=(t=itype =(%disjoint (union-relate first (import-type-pattern t))))) |
6592 $(cases t.cases)
6420 $(cases t.cases)
6594−++ find-imported-mold-prelude
6422+++ find-imported-mold
6595− |= [module=term name=term externals=iexternals surs=(list term) prelude=ifile]
6423+ |= [module=term name=term externals=iexternals surs=(list term)]
6596 ^- (unit itype)
6424 ^- (unit itype)
6597− =/ standard=(unit ischeme) (find-jibb-mold %unit prelude)
6598 ?. (lien surs |=(n=term =(n module))) ~
6425 ?. (lien surs |=(n=term =(n module))) ~
6599 =/ found=iexternals
6426 =/ found=iexternals
6600 (skim externals |=(e=[module=term name=term result=*] &(=(module module.e) =(name name.e))))
6427 (skim externals |=(e=[module=term name=term result=*] &(=(module module.e) =(name name.e))))
@@ -6605,17 +6432,13 @@
6605 ?. ?=(%& -.result) ~
6432 ?. ?=(%& -.result) ~
6606 =/ node=* +.result
6433 =/ node=* +.result
6607 ?. (imported-faces-valid node) ~
6434 ?. (imported-faces-valid node) ~
6608− ?@ node (import-to-itype-standard node standard)
6435+ ?@ node (import-to-itype node)
6609− ?: ?=(%ref -.node) (import-to-itype-standard node standard)
6436+ ?: ?=(%ref -.node) (import-to-itype node)
6610 =/ pattern=(unit irec-pattern) (rec-pattern node module name)
6437 =/ pattern=(unit irec-pattern) (rec-pattern node module name)
6611− ?~ pattern (import-to-itype-standard node standard)
6438+ ?~ pattern (import-to-itype node)
6612− ?. has.u.pattern (import-to-itype-standard node standard)
6439+ ?. has.u.pattern (import-to-itype node)
6613 `[%recursive module name `(crip "{(trip name)}.{(trip module)}")]
6440 `[%recursive module name `(crip "{(trip name)}.{(trip module)}")]
6615−++ find-imported-mold
6616− |= [module=term name=term externals=iexternals surs=(list term)]
6618− (find-imported-mold-prelude module name externals surs *ifile)
6620++ collect-sur-imports
6443++ collect-sur-imports
6621 |= imports=(list import)
6444 |= imports=(list import)
@@ -6633,10 +6456,9 @@
6633 [mark.i.imports $(imports t.imports)]
6456 [mark.i.imports $(imports t.imports)]
6634 $(imports t.imports)
6457 $(imports t.imports)
6636−++ find-imported-mark-prelude
6459+++ find-imported-mark
6637− |= [name=term externals=imark-externals marks=(list term) prelude=ifile]
6460+ |= [name=term externals=imark-externals marks=(list term)]
6638 ^- (unit itype)
6461 ^- (unit itype)
6639− =/ standard=(unit ischeme) (find-jibb-mold %unit prelude)
6640 ?. (unique-value-name name marks) ~
6462 ?. (unique-value-name name marks) ~
6641 =/ found=imark-externals
6463 =/ found=imark-externals
6642 (skim externals |=(e=[mark=term result=*] =(name mark.e)))
6464 (skim externals |=(e=[mark=term result=*] =(name mark.e)))
@@ -6646,12 +6468,7 @@
6646 ?@ result ~
6468 ?@ result ~
6647 ?. ?=(%& -.result) ~
6469 ?. ?=(%& -.result) ~
6648 ?. (imported-faces-valid +.result) ~
6470 ?. (imported-faces-valid +.result) ~
6649− (import-to-itype-standard +.result standard)
6471+ (import-to-itype +.result)
6651−++ find-imported-mark
6652− |= [name=term externals=imark-externals marks=(list term)]
6654− (find-imported-mark-prelude name externals marks *ifile)
6656++ find-jibb-interface
6473++ find-jibb-interface
6657 |= [face=term imports=ijimports]
6474 |= [face=term imports=ijimports]
@@ -6805,27 +6622,15 @@
6805 ?~ rest ~
6622 ?~ rest ~
6806 `[[i.names i.args] u.rest]
6623 `[[i.names i.args] u.rest]
6808−++ template-apply-sub
6625+++ template-apply
6809− |= [template=ischeme args=(list itype) sub=isub]
6626+ |= [template=ischeme args=(list itype)]
6810− ^- (unit [typ=itype sub=isub])
6627+ ^- (unit itype)
6811 =/ vars=(list @ud) vars.template
6628 =/ vars=(list @ud) vars.template
6812 =/ ren=isub ~
6629 =/ ren=isub ~
6814− ?~ vars ?~(args `[(itype-rename typ.template ren) sub] ~)
6631+ ?~ vars ?~(args `(itype-rename typ.template ren) ~)
6815 ?~ args ~
6632 ?~ args ~
6816− =/ replacement=(unit igf-form)
6817− ?: (itype-var-is-gate-free i.vars typ.template)
6818− (itype-gate-free-form i.args sub 256)
6821− $(vars t.vars, args t.args, ren [[i.vars typ.u.replacement] ren], sub sub.u.replacement)
6633+ $(vars t.vars, args t.args, ren [[i.vars i.args] ren])
6824− |= [template=ischeme args=(list itype)]
6826− =/ applied=(unit [typ=itype sub=isub]) (template-apply-sub template args ~)
6830++ infer-shape-args
6635++ infer-shape-args
6831 |= [args=(list shape) state=istate]
6636 |= [args=(list shape) state=istate]
@@ -7066,12 +6871,12 @@
7066 ?^ vars.u.found ~
6871 ?^ vars.u.found ~
7067 `[(itype-in-import typ.u.found u.iface i.t.names.sh prelude.state) state]
6872 `[(itype-in-import typ.u.found u.iface i.t.names.sh prelude.state) state]
7068 =/ found=(unit itype)
6873 =/ found=(unit itype)
7069− (find-imported-mold-prelude i.t.names.sh n externals.state surs.state ?~(prelude.state *ifile u.prelude.state))
6874+ (find-imported-mold i.t.names.sh n externals.state surs.state)
7070 ?~ found ~
6875 ?~ found ~
7071 `[u.found state]
6876 `[u.found state]
7072 ?: (lien marks.state |=(x=term =(x n)))
6877 ?: (lien marks.state |=(x=term =(x n)))
7073 ?^ (find-simple-mold n molds.state) ~
6878 ?^ (find-simple-mold n molds.state) ~
7074− =/ imported=(unit itype) (find-imported-mark-prelude n mark-externals.state marks.state ?~(prelude.state *ifile u.prelude.state))
6879+ =/ imported=(unit itype) (find-imported-mark n mark-externals.state marks.state)
7075 ?~ imported ~
6880 ?~ imported ~
7076 `[u.imported state]
6881 `[u.imported state]
7077 ?: (lien active.state |=(x=term =(x n))) ~
6882 ?: (lien active.state |=(x=term =(x n))) ~
@@ -7095,17 +6900,6 @@
7095 =/ args=(unit [types=(list itype) state=istate]) (infer-shape-args args.sh state)
6900 =/ args=(unit [types=(list itype) state=istate]) (infer-shape-args args.sh state)
7096 ?~ args ~
6901 ?~ args ~
7097 =/ n=term i.ref.sh
6902 =/ n=term i.ref.sh
7098− =/ keyed=(unit [types=(list itype) sub=isub])
7099− ?: ?=(^ (find-simple-mold n molds.state.u.args))
7100− `[types.u.args sub.state.u.args]
7101− ?~ prelude.state.u.args
7102− (itype-collection-keys n types.u.args sub.state.u.args)
7103− ?: ?=(^ (find-jibb-mold n u.prelude.state.u.args))
7104− `[types.u.args sub.state.u.args]
7105− (itype-collection-keys n types.u.args sub.state.u.args)
7107− =. types.u.args types.u.keyed
7108− =. sub.state.u.args sub.u.keyed
7109 ?^ t.ref.sh
6903 ?^ t.ref.sh
7110 ?^ t.t.ref.sh ~
6904 ?^ t.t.ref.sh ~
7111 =/ iface=(unit ifile) (find-jibb-interface i.t.ref.sh jimports.state.u.args)
6905 =/ iface=(unit ifile) (find-jibb-interface i.t.ref.sh jimports.state.u.args)
@@ -7113,10 +6907,9 @@
7113 =/ template=(unit ischeme) (find-jibb-mold n u.iface)
6907 =/ template=(unit ischeme) (find-jibb-mold n u.iface)
7114 ?~ template ~
6908 ?~ template ~
7115 ?~ vars.u.template ~
6909 ?~ vars.u.template ~
7116− =/ applied=(unit [typ=itype sub=isub]) (template-apply-sub u.template types.u.args sub.state.u.args)
6910+ =/ applied=(unit itype) (template-apply u.template types.u.args)
7117 ?~ applied ~
6911 ?~ applied ~
7118− =. sub.state.u.args sub.u.applied
7119− `[(itype-in-import typ.u.applied u.iface i.t.ref.sh prelude.state.u.args) state.u.args]
6912+ `[(itype-in-import u.applied u.iface i.t.ref.sh prelude.state.u.args) state.u.args]
7120 ?: (lien active.state.u.args |=(x=term =(x n))) ~
6913 ?: (lien active.state.u.args |=(x=term =(x n))) ~
7121 =/ found=(unit shape) (find-simple-mold n molds.state.u.args)
6914 =/ found=(unit shape) (find-simple-mold n molds.state.u.args)
7122 ?~ found
6915 ?~ found
@@ -7125,10 +6918,9 @@
7125 =/ prelude-entry=(unit ischeme) (find-jibb-mold n u.prelude.state.u.args)
6918 =/ prelude-entry=(unit ischeme) (find-jibb-mold n u.prelude.state.u.args)
7126 ?~ prelude-entry ~
6919 ?~ prelude-entry ~
7127 ?~ vars.u.prelude-entry ~
6920 ?~ vars.u.prelude-entry ~
7128− =/ applied=(unit [typ=itype sub=isub]) (template-apply-sub u.prelude-entry types.u.args sub.state.u.args)
6921+ =/ applied=(unit itype) (template-apply u.prelude-entry types.u.args)
7129 ?~ applied ~
6922 ?~ applied ~
7130− =. sub.state.u.args sub.u.applied
7131− `[typ.u.applied state.u.args]
6923+ `[u.applied state.u.args]
7132 ?. ?=(%generic -.u.found) ~
6924 ?. ?=(%generic -.u.found) ~
7133 =/ grec=(unit itype) (simple-source-generic-recursive n u.found types.u.args state.u.args)
6925 =/ grec=(unit itype) (simple-source-generic-recursive n u.found types.u.args state.u.args)
7134 ?^ grec `[u.grec state.u.args]
6926 ?^ grec `[u.grec state.u.args]
@@ -7437,115 +7229,10 @@
7437 ^- istate
7229 ^- istate
7438 (reserve-cap-sites (scope-expr e) state)
7230 (reserve-cap-sites (scope-expr e) state)
7440−:: +definite-diag: whether a failure is an error in the program itself
7442−:: A definite error names the sites that conflict. A form partial
7443−:: inference does not support names none, and neither does a name
7444−:: that is not inferred yet, such as a sibling that waits for a later
7445−:: pass. An uncertain hole is the one unsupported result with a site.
7451− !=(msg.diag uncertain-hole-msg)
7453−:: +shared-types: what a body's shared variables resolve to
7455−:: The variables free in env or in the enclosing capitals, such as an
7456−:: enclosing gate's untyped sample, are shared by all of the body's
7457−:: locals. A local keeps monomorphic only the variables that these
7458−:: resolve to; it generalizes the rest, which each use renames.
7461− |= [env=ienv caps=icaps sub=isub]
7462− ^- (list [id=@ud typ=itype])
7464− (unique-type-vars (weld (free-env-vars env sub) (free-cap-vars caps sub)))
7465− |=(id=@ud [id (itype-normalize [%var id] sub)])
7467−:: +shared-moved: whether a sibling bound or refined a shared variable
7469−:: A sibling that infers can constrain a shared variable and so turn
7470−:: another local's failure into a success: +itype-fit accepts any type
7471−:: it can prove empty, so after `^- !! x` every cast of x fits. Such a
7472−:: failure can depend on the order siblings are tried in. A variable
7473−:: that a sibling keeps monomorphic occurs in what a shared variable
7474−:: resolves to, so constraining it moves a shared variable too. A
7475−:: substitution only grows, so when none moved, every sibling inferred
7476−:: so far, and the local, ran against the entry state and generalized
7480− |= [shared=(list [id=@ud typ=itype]) sub=isub]
7482− (lien shared |=([id=@ud typ=itype] !=(typ (itype-normalize [%var id] sub))))
7484−:: +closed-local: whether a local cannot see any shared variable
7486−:: A local that names no sibling, itself included, no name whose type
7487−:: had a free variable when the body was entered, and no enclosing
7488−:: capital that did, is inferred from generalized schemes and known
7489−:: types alone. What its siblings do cannot change its result, so its
7490−:: error is its own in any order. +sub is the substitution on entry,
7491−:: since a sibling may since have bound such a variable. The names are
7492−:: syntactic and ignore binders, so this errs closed.
7495− |= [d=def siblings=(list term) env=ienv caps=icaps sub=isub]
7497− ?. ?=(%value -.d) |
7498− =/ deps=(list term) (dependency-expr val.d)
7499− ?: (lien deps |=(n=term |(=(n name.d) (lien siblings |=(s=term =(s n)))))) |
7502− =/ sc=(unit ischeme) (ienv-lookup n env)
7504− ?=(^ (free-env-vars ~[[n u.sc]] sub))
7506− %+ levy (scope-expr val.d)
7508− =/ id=(unit @ud) (icap-lookup name.site caps)
7510− ?=(~ (itype-vars (itype-normalize [%var u.id] sub)))
7512−:: +infer-local-defs: infer a body's local values in dependency order
7514−:: A definition that fails, or whose type is still pending, waits for
7515−:: the next pass, since it may refer to a sibling inferred later. When
7516−:: a pass makes no progress and no cyclic group applies, report the
7517−:: definite error of the earliest waiting definition, if no order of
7518−:: the siblings could change it; otherwise the message stays generic.
7520−:: A failure counts only if it names its sites. The failure of a
7521−:: local that sees no shared variable (+closed-local) is its own. Any
7522−:: other failure counts only if no shared variable had moved when it
7523−:: was tried, and, when the body has shared variables, every other
7524−:: waiting definition also failed with sites: one that waits without
7525−:: them, on a checker limit, a pending tag or its own nested stall,
7526−:: might in another order, or once supported, constrain a shared
7527−:: variable and so let the failing local pass. When all of them failed
7528−:: with sites and none moved a shared variable, the state is the same
7529−:: in every order. With no shared variables, each local is inferred
7530−:: from generalized schemes alone.
7532−:: A cyclic group's own errors are not kept. A definition that infers
7533−:: but is then unsupported reports that at once: a failure recorded
7534−:: earlier in the pass may still pass on a retry, once a sibling has
7535−:: constrained a shared variable.
7537++ infer-local-defs
7232++ infer-local-defs
7538 |= [ds=(list def) env=ienv state=istate]
7233 |= [ds=(list def) env=ienv state=istate]
7539 ^- ilocal-result
7234 ^- ilocal-result
7540− =/ shared=(list [id=@ud typ=itype]) (shared-types env caps.state sub.state)
7541 =/ remaining=(list def) ~
7235 =/ remaining=(list def) ~
7542− =/ siblings=(list term) (global-value-names ds)
7543− =/ entry=isub sub.state
7544− :: this pass's failures with sites that are closed or were tried before
7545− :: any shared variable moved, newest first; and whether a definition
7546− :: waits without sites
7547− =/ failures=(list [diag=idiag closed=?]) ~
7549 =/ progressed=? |
7236 =/ progressed=? |
@@ -7555,35 +7242,16 @@
7555 =/ groups=icomponents (graph-components pending (global-value-names pending))
7242 =/ groups=icomponents (graph-components pending (global-value-names pending))
7556 =/ grouped=(unit [rest=(list def) env=ienv state=istate])
7243 =/ grouped=(unit [rest=(list def) env=ienv state=istate])
7557 (try-local-group pending groups env state)
7244 (try-local-group pending groups env state)
7559− =/ sure=(list [diag=idiag closed=?])
7560− ?: |(?=(~ shared) !blocked) failures
7561− (skim failures |=([diag=idiag closed=?] closed))
7562− ?^ sure [%| diag:(rear sure)]
7563− [%| ["local definitions need unsupported inference" ~]]
7245+ ?~ grouped [%| ["local definitions need unsupported inference" ~]]
7564− $(ds rest.u.grouped, remaining ~, failures ~, blocked |, env env.u.grouped, state state.u.grouped, progressed |)
7246+ $(ds rest.u.grouped, remaining ~, env env.u.grouped, state state.u.grouped, progressed |)
7565− $(ds (flop remaining), remaining ~, failures ~, blocked |, progressed |)
7247+ $(ds (flop remaining), remaining ~, progressed |)
7566 =/ d=def i.ds
7248 =/ d=def i.ds
7567 ?> ?=(%value -.d)
7249 ?> ?=(%value -.d)
7568 =/ local-state=istate (reserve-def-caps val.d state)
7250 =/ local-state=istate (reserve-def-caps val.d state)
7569− =/ plain=iresult (infer-fragment val.d env local-state)
7251+ =/ inferred=iresult (infer-fragment val.d env local-state)
7570− =/ inferred=iresult
7252+ =/ retried=? ?=(%| -.inferred)
7571− ?: ?=(%& -.plain) plain
7572− (infer-recursive-gate d env local-state)
7253+ =? inferred retried (infer-recursive-gate d env local-state)
7573− ?: ?=(%| -.inferred)
7574− :: For a value that is not a gate the retry only says so; keep the
7575− :: first failure unless the retry found a definite error.
7577− ?: ?=(%& -.plain) p.inferred
7578− ?: (definite-diag p.inferred) p.inferred
7580− ?. (definite-diag failure) $(ds t.ds, remaining [d remaining], blocked &)
7581− =/ closed=? (closed-local d siblings env caps.state entry)
7582− =? failures |(closed !(shared-moved shared sub.state))
7583− [[failure closed] failures]
7584− $(ds t.ds, remaining [d remaining])
7254+ ?: ?=(%| -.inferred) $(ds t.ds, remaining [d remaining])
7585− :: Only the deferred transaction adds obligations, and it keeps no
7586− :: failure reason. Obligations from a local are a checker limit.
7587 ?: !=(obligations.state.p.inferred obligations.state) [%| ["deferred local definition needs unsupported inference" ~]]
7255 ?: !=(obligations.state.p.inferred obligations.state) [%| ["deferred local definition needs unsupported inference" ~]]
7588 =. state.p.inferred (promote-restricted-numbers state.p.inferred env)
7256 =. state.p.inferred (promote-restricted-numbers state.p.inferred env)
7589 =. state.p.inferred (default-hole-numbers holes.state.p.inferred holes.state state.p.inferred env !(itype-has-gate (itype-normalize typ.p.inferred sub.state.p.inferred)))
7257 =. state.p.inferred (default-hole-numbers holes.state.p.inferred holes.state state.p.inferred env !(itype-has-gate (itype-normalize typ.p.inferred sub.state.p.inferred)))
@@ -7597,9 +7265,9 @@
7597 [%| ["explicit capital constraints are not supported by partial inference" ~]]
7265 [%| ["explicit capital constraints are not supported by partial inference" ~]]
7598 =/ typ=itype (itype-normalize typ.p.inferred sub.state.p.inferred)
7266 =/ typ=itype (itype-normalize typ.p.inferred sub.state.p.inferred)
7599 ?: |((pending-tags tags.state.p.inferred sub.state.p.inferred) (itype-has-tag typ))
7267 ?: |((pending-tags tags.state.p.inferred sub.state.p.inferred) (itype-has-tag typ))
7600− $(ds t.ds, remaining [d remaining], blocked &)
7268+ $(ds t.ds, remaining [d remaining])
7601 ?: (unsupported-atom-vars typ caps.state.p.inferred binders.state.p.inferred sub.state.p.inferred)
7269 ?: (unsupported-atom-vars typ caps.state.p.inferred binders.state.p.inferred sub.state.p.inferred)
7602− $(ds t.ds, remaining [d remaining], blocked &)
7270+ $(ds t.ds, remaining [d remaining])
7603 =/ free=(list @ud)
7271 =/ free=(list @ud)
7604 (weld (free-env-vars env sub.state.p.inferred) (free-cap-vars caps.state sub.state.p.inferred))
7272 (weld (free-env-vars env sub.state.p.inferred) (free-cap-vars caps.state sub.state.p.inferred))
7605 =/ vars=(list @ud) (unique-type-vars (itype-vars typ))
7273 =/ vars=(list @ud) (unique-type-vars (itype-vars typ))
@@ -7809,12 +7477,7 @@
7809 =/ target=itype (itype-walk expected sub.state)
7477 =/ target=itype (itype-walk expected sub.state)
7810 =/ value=iresult (infer-call-context-arg i.items target env state context)
7478 =/ value=iresult (infer-call-context-arg i.items target env state context)
7811 ?: ?=(%| -.value) value
7479 ?: ?=(%| -.value) value
7812− =/ ordinary-fit=ifit (itype-fit typ.p.value target sub.state.p.value next.state.p.value)
7480+ =/ fit=ifit (itype-fit typ.p.value target sub.state.p.value next.state.p.value)
7814− ?: ?=(%ok -.ordinary-fit) ordinary-fit
7815− ?: ?&(?=(%union -.target) ?=(^ prelude.state) =(origin.target `[at.u.prelude.state %element]))
7816− (program-single-generic-fit typ.p.value target sub.state.p.value next.state.p.value)
7818 ?: ?=(%unknown -.fit) [%| ["list item constraint is not supported by partial inference" ~]]
7481 ?: ?=(%unknown -.fit) [%| ["list item constraint is not supported by partial inference" ~]]
7819 ?: ?=(%bad -.fit)
7482 ?: ?=(%bad -.fit)
7820 ?: |((itype-family-related typ.p.value target sub.state.p.value) (itype-has-any-atom typ.p.value sub.state.p.value) (itype-has-any-atom target sub.state.p.value))
7483 ?: |((itype-family-related typ.p.value target sub.state.p.value) (itype-has-any-atom typ.p.value sub.state.p.value) (itype-has-any-atom target sub.state.p.value))
@@ -7831,12 +7494,7 @@
7831 =/ target=itype (itype-walk expected sub.state)
7494 =/ target=itype (itype-walk expected sub.state)
7832 =/ value=iresult (infer-call-context-arg i.items target env state context)
7495 =/ value=iresult (infer-call-context-arg i.items target env state context)
7833 ?: ?=(%| -.value) value
7496 ?: ?=(%| -.value) value
7834− =/ ordinary-fit=ifit (itype-fit typ.p.value target sub.state.p.value next.state.p.value)
7497+ =/ fit=ifit (itype-fit typ.p.value target sub.state.p.value next.state.p.value)
7836− ?: ?=(%ok -.ordinary-fit) ordinary-fit
7837− ?: ?&(?=(%union -.target) ?=(^ prelude.state) =(origin.target `[at.u.prelude.state %element]))
7838− (program-single-generic-fit typ.p.value target sub.state.p.value next.state.p.value)
7840 ?: ?=(%unknown -.fit) [%| ["list item constraint is not supported by partial inference" ~]]
7498 ?: ?=(%unknown -.fit) [%| ["list item constraint is not supported by partial inference" ~]]
7841 ?: ?=(%bad -.fit)
7499 ?: ?=(%bad -.fit)
7842 =/ missing=(unit idiag) (missing-union-tag i.items target sub.state.p.value context)
7500 =/ missing=(unit idiag) (missing-union-tag i.items target sub.state.p.value context)
@@ -8704,8 +8362,8 @@
8704 %duration [%& [%atom %dr] state]
8362 %duration [%& [%atom %dr] state]
8705 %knot [%& [%atom %ta] state]
8363 %knot [%& [%atom %ta] state]
8706 %loobean [%& [%flag ~] state]
8364 %loobean [%& [%flag ~] state]
8707− %term [%& [%tag next.state lit.e |] state(next +(next.state), tags [[next.state lit.e at.e] tags.state])]
8365+ %term [%& [%tag next.state lit.e |] state(next +(next.state), tags [[next.state lit.e] tags.state])]
8708− %null [%& [%tag next.state lit.e |] state(next +(next.state), tags [[next.state lit.e at.e] tags.state])]
8366+ %null [%& [%tag next.state lit.e |] state(next +(next.state), tags [[next.state lit.e] tags.state])]
8711 ?~ prelude.state [%| ["unit construction needs the standard prelude in partial inference" ~]]
8369 ?~ prelude.state [%| ["unit construction needs the standard prelude in partial inference" ~]]
@@ -8772,15 +8430,12 @@
8772 =/ target=iresult $(e [%wing at.e target.e])
8430 =/ target=iresult $(e [%wing at.e target.e])
8773 ?: ?=(%| -.target) target
8431 ?: ?=(%| -.target) target
8774 (infer-change-edits edits.e typ.p.target env state.p.target ~)
8432 (infer-change-edits edits.e typ.p.target env state.p.target ~)
8775− %ctor [%& [%tag next.state tag.e &] state(next +(next.state), tags [[next.state tag.e at.e] tags.state])]
8433+ %ctor [%& [%tag next.state tag.e &] state(next +(next.state), tags [[next.state tag.e] tags.state])]
8777 =/ traced=iresult $(e val.e)
8435 =/ traced=iresult $(e val.e)
8778 ?: ?=(%| -.traced) traced
8436 ?: ?=(%| -.traced) traced
8779 $(e then.e, state state.p.traced)
8437 $(e then.e, state state.p.traced)
8781− ?: &(?=(^ defer.state) ?=(^ prelude.state))
8782− (dg-infer-tuple-items items.e env state)
8783− (infer-simple-items items.e env state)
8438+ %tuple (infer-simple-items items.e env state)
8785 ?~ defs.e $(e final.e)
8440 ?~ defs.e $(e final.e)
8786 =/ local-names=(list term) (global-value-names defs.e)
8441 =/ local-names=(list term) (global-value-names defs.e)
@@ -9304,17 +8959,7 @@
9304 ?~ args.result |
8959 ?~ args.result |
9305 ?. =((lent args.result) (lent args.expected)) |
8960 ?. =((lent args.result) (lent args.expected)) |
9306 ?: |((itype-has-tag (itype-normalize result sub.state.p.head)) (itype-has-tag (itype-normalize expected sub.state.p.head))) |
8961 ?: |((itype-has-tag (itype-normalize result sub.state.p.head)) (itype-has-tag (itype-normalize expected sub.state.p.head))) |
9307− =/ result-recursive=? (itype-has-recursive (itype-normalize result sub.state.p.head))
9308− =/ expected-recursive=? (itype-has-recursive (itype-normalize expected sub.state.p.head))
8962+ ?: |((itype-has-recursive (itype-normalize result sub.state.p.head)) (itype-has-recursive (itype-normalize expected sub.state.p.head))) |
9310− ?. result-recursive &
9312− &(=(at.u.prelude.state /lib/jibb/prelude/jibb) =(origin.result `[at.u.prelude.state %element]))
9314− ?. expected-recursive &
9316− &(=(at.u.prelude.state /lib/jibb/prelude/jibb) =(origin.expected `[at.u.prelude.state %element]))
9317− ?. &(result-ok expected-ok) |
9318 ?: |((itype-has-any-atom result sub.state.p.head) (itype-has-any-atom expected sub.state.p.head)) |
8963 ?: |((itype-has-any-atom result sub.state.p.head) (itype-has-any-atom expected sub.state.p.head)) |
9320 ?. eligible (infer-call-with-head e env state head)
8965 ?. eligible (infer-call-with-head e env state head)
@@ -9596,8 +9241,6 @@
9596 |= [e=expr expected=itype env=ienv state=istate context=span]
9241 |= [e=expr expected=itype env=ienv state=istate context=span]
9597 ^- iresult
9242 ^- iresult
9598 ?: &(?=(^ defer.state) ?=(%branch -.e)) (infer-fragment e env state)
9243 ?: &(?=(^ defer.state) ?=(%branch -.e)) (infer-fragment e env state)
9599− ?: &(?=(^ defer.state) ?=(^ prelude.state) ?=(%tuple -.e))
9600− (infer-fragment e env state)
9601 ?: ?=(%pair -.e) $(e (pair-as-cell e))
9244 ?: ?=(%pair -.e) $(e (pair-as-cell e))
9602 ?: ?=(%group -.e) $(e inner.e)
9245 ?: ?=(%group -.e) $(e inner.e)
9603 ?: &(?=(%body -.e) ?=(~ defs.e)) $(e final.e)
9246 ?: &(?=(%body -.e) ?=(~ defs.e)) $(e final.e)
@@ -9866,9 +9509,6 @@
9867 ?: (lth id.t 26) [(add 65 id.t) ~]
9510 ?: (lth id.t 26) [(add 65 id.t) ~]
9868 "T{<id.t>}"
9511 "T{<id.t>}"
9870− ?: (lth id.t 26) [(add 65 id.t) ~]
9873 ?: (lth id.t 26) [(add 65 id.t) ~]
9513 ?: (lth id.t 26) [(add 65 id.t) ~]
9874 "T{<id.t>}"
9514 "T{<id.t>}"
@@ -9932,7 +9572,6 @@
9933 %rnvar &
9573 %rnvar &
@@ -9956,7 +9595,7 @@
9956 |= [label=tape typ=itype sub=isub]
9595 |= [label=tape typ=itype sub=isub]
9958 =/ normalized=itype (itype-normalize typ sub)
9597 =/ normalized=itype (itype-normalize typ sub)
9959− ?: |(?=(%var -.normalized) ?=(%fvar -.normalized) ?=(%avar -.normalized) ?=(%rvar -.normalized) (itype-has-nvar normalized) (itype-has-tag normalized) (itype-has-union normalized)) label
9598+ ?: |(?=(%var -.normalized) ?=(%avar -.normalized) ?=(%rvar -.normalized) (itype-has-nvar normalized) (itype-has-tag normalized) (itype-has-union normalized)) label
9960 ?: (itype-has-hidden-recursive normalized) label
9599 ?: (itype-has-hidden-recursive normalized) label
9961 =/ vars=(list @ud) (unique-type-vars (itype-vars normalized))
9600 =/ vars=(list @ud) (unique-type-vars (itype-vars normalized))
9962 ?: (gth (lent vars) 26) label
9601 ?: (gth (lent vars) 26) label
@@ -9977,7 +9616,6 @@
9977 =/ ident=(unit @ud)
9616 =/ ident=(unit @ud)
9978 ?+ -.resolved ~
9617 ?+ -.resolved ~
9979 %var `id.resolved
9618 %var `id.resolved
9981 %avar `id.resolved
9619 %avar `id.resolved
9982 %rvar `id.resolved
9620 %rvar `id.resolved
@@ -9993,7 +9631,6 @@
9993 =/ ident=(unit @ud)
9631 =/ ident=(unit @ud)
9994 ?+ -.resolved ~
9632 ?+ -.resolved ~
9995 %var `id.resolved
9633 %var `id.resolved
9997 %avar `id.resolved
9634 %avar `id.resolved
9998 %rvar `id.resolved
9635 %rvar `id.resolved
@@ -10009,7 +9646,6 @@
10009 =/ ident=(unit @ud)
9646 =/ ident=(unit @ud)
10010 ?+ -.resolved ~
9647 ?+ -.resolved ~
10011 %var `id.resolved
9648 %var `id.resolved
10012− %fvar `id.resolved
10013 %avar `id.resolved
9649 %avar `id.resolved
10014 %rvar `id.resolved
9650 %rvar `id.resolved
@@ -10026,7 +9662,6 @@
10026 =/ ident=(unit @ud)
9662 =/ ident=(unit @ud)
10027 ?+ -.resolved ~
9663 ?+ -.resolved ~
10028 %var `id.resolved
9664 %var `id.resolved
10029− %fvar `id.resolved
10030 %avar `id.resolved
9665 %avar `id.resolved
10031 %rvar `id.resolved
9666 %rvar `id.resolved
@@ -10053,7 +9688,6 @@
10057 %avar =(n id.t)
9691 %avar =(n id.t)
10058 %rvar =(n id.t)
9692 %rvar =(n id.t)
10059 %nvar |
9693 %nvar |
@@ -10116,10 +9750,6 @@
10116 =/ sep=tape ?:(printed ", " " where ")
9750 =/ sep=tape ?:(printed ", " " where ")
10117 =/ clause=tape "{sep}{(show-itype [%avar i.vars] ~)} is an atom"
9751 =/ clause=tape "{sep}{(show-itype [%avar i.vars] ~)} is an atom"
10118 $(vars t.vars, printed &, out (weld out clause))
9752 $(vars t.vars, printed &, out (weld out clause))
10119− ?: (itype-var-is-gate-free i.vars t)
10120− =/ sep=tape ?:(printed ", " " where ")
10121− =/ clause=tape "{sep}{(show-itype [%fvar i.vars] ~)} contains no gates"
10122− $(vars t.vars, printed &, out (weld out clause))
10123 $(vars t.vars)
9753 $(vars t.vars)
10125:: Build the supported part of the value environment in dependency order.
9755:: Build the supported part of the value environment in dependency order.
@@ -10480,6 +10110,11 @@
10480 =. entry entry(source src, target dst)
10110 =. entry entry(source src, target dst)
10481 `[entry u.rest]
10111 `[entry u.rest]
10113+++ add-supported-defs
10114+ |= [ds=(list def) all-defs=(list def) checked=(map term def) heads=(unit igate-prelude-evidence) env=ienv molds=imolds globals=(list term) externals=iexternals surs=(list term) mark-externals=imark-externals marks=(list term) jimports=ijimports reserved-molds=(list term) at=path prelude=(unit ifile) artifacts=(list iwidth-definition)]
10115+ ^- [env=ienv artifacts=(list iwidth-definition)]
10116+ (add-supported-defs-core ds all-defs checked heads env molds globals externals surs mark-externals marks jimports reserved-molds at prelude artifacts ~)
10484+$ iresolved [env=ienv grouped=(list term) artifacts=(list iwidth-definition)]
10119+$ iresolved [env=ienv grouped=(list term) artifacts=(list iwidth-definition)]
10485+$ iadj (map term (list term))
10120+$ iadj (map term (list term))
@@ -10597,31 +10232,8 @@
10597 (resolve-groups-core ds molds globals externals surs mark-externals marks jimports reserved-molds at prelude ~)
10232 (resolve-groups-core ds molds globals externals surs mark-externals marks jimports reserved-molds at prelude ~)
10600−+$ iadded-definition
10601− [env=ienv checked=(map term def) artifacts=(list iwidth-definition)]
10602−++ add-supported-result
10603− |= [d=def result=iresult initial=istate env=ienv checked=(map term def) artifacts=(list iwidth-definition)]
10604− ^- (unit iadded-definition)
10606− ?: ?=(%| -.result) ~
10607− =. state.p.result (promote-restricted-numbers state.p.result env)
10608− =. state.p.result (default-hole-numbers holes.state.p.result holes.initial state.p.result env !(itype-has-gate (itype-normalize typ.p.result sub.state.p.result)))
10609− ?^ (unresolved-hole holes.state.p.result holes.initial state.p.result) ~
10610− ?: (constrained-capitals caps.state.p.result sub.state.p.result) ~
10611− =/ typ=itype (default-decimals (itype-normalize typ.p.result sub.state.p.result))
10612− ?: |((pending-tags tags.state.p.result sub.state.p.result) (itype-has-tag typ)) ~
10613− ?: (unsupported-atom-vars typ caps.state.p.result binders.state.p.result sub.state.p.result) ~
10614− =/ vars=(list @ud) (unique-type-vars (itype-vars typ))
10615− ?: (gth (lent vars) 26) ~
10616− =/ finalized=(unit (list iwprojection))
10617− (width-finalize projections.state.p.result sub.state.p.result vars)
10619− =? artifacts ?=(^ u.finalized)
10620− [[name.d val.d typ sub.state.p.result (flop u.finalized)] artifacts]
10621− =? checked |(?=(%gate -.val.d) ?=(%gate-wide -.val.d)) (~(put by checked) name.d d)
10622− `[[[name.d [typ vars]] env] checked artifacts]
10623++ add-supported-defs-core
10235++ add-supported-defs-core
10624− |= [ds=(list def) checked=(map term def) heads=(unit igate-prelude-evidence) env=ienv molds=imolds globals=(list term) externals=iexternals surs=(list term) mark-externals=imark-externals marks=(list term) jimports=ijimports reserved-molds=(list term) at=path prelude=(unit ifile) artifacts=(list iwidth-definition) index=(unit [at=path source=@t prelude=ifile shapes=(map term shape)])]
10236+ |= [ds=(list def) all-defs=(list def) checked=(map term def) heads=(unit igate-prelude-evidence) env=ienv molds=imolds globals=(list term) externals=iexternals surs=(list term) mark-externals=imark-externals marks=(list term) jimports=ijimports reserved-molds=(list term) at=path prelude=(unit ifile) artifacts=(list iwidth-definition) index=(unit [at=path source=@t prelude=ifile shapes=(map term shape)])]
10625 ^- [env=ienv artifacts=(list iwidth-definition)]
10237 ^- [env=ienv artifacts=(list iwidth-definition)]
10626 ?~ ds [env artifacts]
10238 ?~ ds [env artifacts]
10627 =/ d=def i.ds
10239 =/ d=def i.ds
@@ -10636,35 +10248,23 @@
10636 =. initial (reserve-def-caps val.d initial)
10248 =. initial (reserve-def-caps val.d initial)
10637 =/ result=iresult (infer-fragment val.d env initial)
10249 =/ result=iresult (infer-fragment val.d env initial)
10638 =? result ?=(%| -.result) (infer-recursive-gate d env initial)
10250 =? result ?=(%| -.result) (infer-recursive-gate d env initial)
10639− =/ added=(unit iadded-definition)
10251+ ?: ?=(%| -.result) $(ds t.ds)
10640− (add-supported-result d result initial env checked artifacts)
10252+ =. state.p.result (promote-restricted-numbers state.p.result env)
10641− ?~ added $(ds t.ds)
10253+ =. state.p.result (default-hole-numbers holes.state.p.result holes.initial state.p.result env !(itype-has-gate (itype-normalize typ.p.result sub.state.p.result)))
10642− $(ds t.ds, env env.u.added, checked checked.u.added, artifacts artifacts.u.added)
10254+ ?^ (unresolved-hole holes.state.p.result holes.initial state.p.result) $(ds t.ds)
10643−::
10255+ ?: (constrained-capitals caps.state.p.result sub.state.p.result) $(ds t.ds)
10644−:: Full checking discards unsupported definitions. On that failure path only,
10256+ =/ typ=itype (default-decimals (itype-normalize typ.p.result sub.state.p.result))
10645−:: retry a bounded number of missing definitions to explain a pending tag
10257+ ?: |((pending-tags tags.state.p.result sub.state.p.result) (itype-has-tag typ)) $(ds t.ds)
10646−:: from the same ordinary inference state instead of hiding it behind the
10258+ ?: (unsupported-atom-vars typ caps.state.p.result binders.state.p.result sub.state.p.result) $(ds t.ds)
10647−:: generic completeness error. No successful definition takes this path.
10259+ =/ vars=(list @ud) (unique-type-vars (itype-vars typ))
10648−++ module-pending-tag
10260+ ?: (gth (lent vars) 26) $(ds t.ds)
10649− |= [ds=(list def) env=ienv base=istate fuel=@ud]
10261+ =/ finalized=(unit (list iwprojection))
10650− ^- (unit [at=span msg=tape])
10262+ (width-finalize projections.state.p.result sub.state.p.result vars)
10651− =/ checked=(map term def) (direct-checked-gates ds env)
10263+ ?~ finalized $(ds t.ds)
10652− =/ heads=(unit igate-prelude-evidence) (direct-prelude-evidence ds prelude.base)
10264+ =? artifacts ?=(^ u.finalized)
10653− |-
10265+ [[name.d val.d typ sub.state.p.result (flop u.finalized)] artifacts]
10654− ?~ ds ~
10266+ =? checked |(?=(%gate -.val.d) ?=(%gate-wide -.val.d)) (~(put by checked) name.d d)
10655− ?: =(0 fuel) ~
10267+ $(ds t.ds, env [[name.d [typ vars]] env], checked checked)
10657− ?: ?=(%mold -.d) $(ds t.ds, fuel (dec fuel))
10658− ?^ (ienv-lookup name.d env) $(ds t.ds, fuel (dec fuel))
10659− =/ initial=istate base(gate-defs checked, head-evidence heads)
10660− =. initial (reserve-def-caps val.d initial)
10661− =/ result=iresult (infer-fragment val.d env initial)
10662− =? result ?=(%| -.result) (infer-recursive-gate d env initial)
10663− ?: ?=(%| -.result) $(ds t.ds, fuel (dec fuel))
10664− =/ pending=(unit [at=span msg=tape])
10665− (pending-tag-diagnostic tags.state.p.result sub.state.p.result)
10666− ?^ pending pending
10667− $(ds t.ds, fuel (dec fuel))
10669++ resolve-groups-core
10269++ resolve-groups-core
10670 |= [ds=(list def) molds=imolds globals=(list term) externals=iexternals surs=(list term) mark-externals=imark-externals marks=(list term) jimports=ijimports reserved-molds=(list term) at=path prelude=(unit ifile) index=(unit [at=path source=@t prelude=ifile shapes=(map term shape)])]
10270 |= [ds=(list def) molds=imolds globals=(list term) externals=iexternals surs=(list term) mark-externals=imark-externals marks=(list term) jimports=ijimports reserved-molds=(list term) at=path prelude=(unit ifile) index=(unit [at=path source=@t prelude=ifile shapes=(map term shape)])]
@@ -10680,7 +10280,7 @@
10680 =/ heads=(unit igate-prelude-evidence) (direct-prelude-evidence ds prelude)
10280 =/ heads=(unit igate-prelude-evidence) (direct-prelude-evidence ds prelude)
10682 =/ next=[env=ienv artifacts=(list iwidth-definition)]
10282 =/ next=[env=ienv artifacts=(list iwidth-definition)]
10683− (add-supported-defs-core ds (direct-checked-gates ds env) heads env molds globals externals surs mark-externals marks jimports reserved-molds at prelude artifacts index)
10283+ (add-supported-defs-core ds ds (direct-checked-gates ds env) heads env molds globals externals surs mark-externals marks jimports reserved-molds at prelude artifacts index)
10684 =/ initial=istate [0 ~ ~ ~ molds globals externals surs mark-externals marks jimports reserved-molds ~ ~ ~ | at top prelude ~ 256 ~ ~ ~ ~ ~ ~]
10284 =/ initial=istate [0 ~ ~ ~ molds globals externals surs mark-externals marks jimports reserved-molds ~ ~ ~ | at top prelude ~ 256 ~ ~ ~ ~ ~ ~]
10685 =. grec-index.initial index
10285 =. grec-index.initial index
10686 =/ out=iresolved (add-groups ds components graph env.next grouped artifacts.next initial)
10286 =/ out=iresolved (add-groups ds components graph env.next grouped artifacts.next initial)
@@ -11046,7 +10646,7 @@
11046++ union-state-leaf
10646++ union-state-leaf
11047 |= t=itype
10647 |= t=itype
11049− ?=(?(%var %fvar %avar %rvar %nvar %rnvar %atom %any-atom %flag %noun %empty %const) -.t)
10649+ ?=(?(%var %avar %rvar %nvar %rnvar %atom %any-atom %flag %noun %empty %const) -.t)
11050++ union-state-params-budget
10650++ union-state-params-budget
11051 |= [params=iparams fuel=@ud]
10651 |= [params=iparams fuel=@ud]
11052 ^- (unit @ud)
10652 ^- (unit @ud)
@@ -11195,22 +10795,6 @@
11195 [at.first at.second (union-relate a (project-union-mold second molds ~))]
10795 [at.first at.second (union-relate a (project-union-mold second molds ~))]
11196 (weld pairs $(cases t.cases))
10796 (weld pairs $(cases t.cases))
11198−:: The partial report and the full module check share one overlap proof,
11199−:: so for the same union both name the same pair. The caller passes the
11200−:: projected .pairs, which the partial report reads again. The projection
11201−:: proves atoms, flags and nested literal cells, and its first overlap is
11202−:: named even when the source slice would prove an earlier pair. The
11203−:: source slice is tried only when some pair is unknown, for its one-hop
11204−:: generic applications. A missing witness does not mean the cases are
11206−++ mold-overlap-witness
11207− |= [cases=(list shape) pairs=(list upair) molds=imolds]
11209− =/ overlapping=(list upair) (skim pairs |=(p=upair =(%overlap relation.p)))
11210− ?^ overlapping `i.overlapping
11211− ?. (lien pairs |=(p=upair =(%unknown relation.p))) ~
11212− (union-source-overlap cases molds 256)
11214:: A closed structural mold supplies no equation to determine a hole.
10798:: A closed structural mold supplies no equation to determine a hole.
11215:: Applications, references, unbound capitals and unions are unproved.
10799:: Applications, references, unbound capitals and unions are unproved.
11216++ simple-mold-hole
10800++ simple-mold-hole
@@ -11350,9 +10934,14 @@
11350 =? sh ?=(%generic -.sh) body.sh
10934 =? sh ?=(%generic -.sh) body.sh
11351 ?. ?=(%union -.sh) (crip "+$ {(trip name.d)}: not checked")
10935 ?. ?=(%union -.sh) (crip "+$ {(trip name.d)}: not checked")
11352 =/ pairs=(list upair) (union-pairs cases.sh molds)
10936 =/ pairs=(list upair) (union-pairs cases.sh molds)
10937+ =/ overlapping=(list upair) (skim pairs |=(p=upair =(%overlap relation.p)))
10939+ ?^ overlapping overlapping
10940+ ?. (lien pairs |=(p=upair =(%unknown relation.p))) ~
11353− =/ witness=(unit upair) (mold-overlap-witness cases.sh pairs molds)
10941+ =/ witness=(unit upair) (union-source-overlap cases.sh molds 256)
11355− =/ p=upair u.witness
10942+ ?~(witness ~ ~[u.witness])
10944+ =/ p=upair i.overlapping
11356 =/ summary=@t (crip "+$ {(trip name.d)}: overlapping cases; mold not checked")
10945 =/ summary=@t (crip "+$ {(trip name.d)}: overlapping cases; mold not checked")
11357 =/ first=@t (show-error src [file line.beg.first.p col.beg.first.p "first union case"])
10946 =/ first=@t (show-error src [file line.beg.first.p col.beg.first.p "first union case"])
11358 =/ second=@t (show-error src [file line.beg.second.p col.beg.second.p "overlapping case"])
10947 =/ second=@t (show-error src [file line.beg.second.p col.beg.second.p "overlapping case"])
@@ -11376,7 +10965,6 @@
11376 (of-wain:format [summary excerpts])
10965 (of-wain:format [summary excerpts])
11378:: Both written field sites are shown in the source that declares them.
10967:: Both written field sites are shown in the source that declares them.
11379−:: A store's derived-name clash shows its two sites the same way.
11380++ show-duplicate-fields
10968++ show-duplicate-fields
11381 |= [file=path src=@t diagnostic=idiag]
10969 |= [file=path src=@t diagnostic=idiag]
@@ -11418,14 +11006,7 @@
11418+$ jbundle (list jsource)
11006+$ jbundle (list jsource)
11419+$ jcache (list [at=path iface=ifile])
11007+$ jcache (list [at=path iface=ifile])
11420+$ jfile-result (each [iface=ifile cache=jcache] @t)
11008+$ jfile-result (each [iface=ifile cache=jcache] @t)
11421−:: Overlap evidence retains the exact source that supplied its spans.
11422−:: Ordinary Jibb imports preserve this evidence through the resolver.
11423−+$ jfile-overlap [file=path source=@t name=term cases=upair]
11424−+$ jfile-failure [message=@t overlap=(unit jfile-overlap)]
11425−+$ jfile-detailed-result (each [iface=ifile cache=jcache] jfile-failure)
11426+$ jimports-result (each [resolved=ijimports cache=jcache] @t)
11009+$ jimports-result (each [resolved=ijimports cache=jcache] @t)
11427−:: Preserve an imported overlap's original file and source across the graph.
11428−+$ jimports-detailed-result (each [resolved=ijimports cache=jcache] jfile-failure)
11430:: Written record fields each have their own lexical record scope.
11011:: Written record fields each have their own lexical record scope.
11431+$ written-fields (map term span)
11012+$ written-fields (map term span)
@@ -11682,44 +11263,22 @@
11682 ?. (levy vals |=(n=term &((unique-value-name n vals) !(lien prelude-values |=(v=term =(n v)))))) |
11263 ?. (levy vals |=(n=term &((unique-value-name n vals) !(lien prelude-values |=(v=term =(n v)))))) |
11683 (levy mold-names |=(n=term &((unique-value-name n mold-names) !(lien prelude-molds |=(m=term =(n m))))))
11264 (levy mold-names |=(n=term &((unique-value-name n mold-names) !(lien prelude-molds |=(m=term =(n m))))))
11685−:: A detailed failure is attached only to the first mold that actually
11266+:: In an API file or before main's kind is known, a lone `+$ poke`
11686−:: failed in this check, using that module's checked source mold table.
11267+:: may be a declaration rather than a mold that shadows the prelude. Do not call
11687−+$ imold-failure [message=@t overlap=(unit [name=term cases=upair])]
11268+:: that one collision definite, and do not hide unrelated scope errors.
11688−:: Validate a generic wrapper without an unbounded duplicate-name pass.
11269+++ pending-declared-poke
11689−++ module-mold-params-valid
11270+ |= [at=path mod=module prelude-values=(list term) prelude-molds=(list term)]
11690− |= [vars=(list @t) seen=(set @t) fuel=@ud]
11692− ?~ vars &
11272+ ?. (lien prelude-molds |=(n=term =(%poke n))) |
11693− ?: =(0 fuel) |
11273+ ?. |(?=([%ui %api @ %jibb ~] at) (lien defs.mod |=(d=def &(?=(%value -.d) =(%main name.d))))) |
11694− ?: (~(has in:..zuse seen) i.vars) |
11274+ =/ pokes=(list def)
11695− $(vars t.vars, seen (~(put in:..zuse seen) i.vars), fuel (dec fuel))
11275+ (skim defs.mod |=(d=def &(?=(%mold -.d) =(%poke name.d))))
11696−++ module-mold-overlap
11276+ ?~ pokes |
11697− |= [m=[name=term body=shape] molds=imolds]
11277+ ?^ t.pokes |
11698− ^- (unit upair)
11278+ =/ remaining=(list def)
11699− =/ sh=shape body.m
11279+ (skim defs.mod |=(d=def !&(?=(%mold -.d) =(%poke name.d))))
11700− =/ valid=?
11280+ (module-scope-valid mod(defs remaining) prelude-values prelude-molds)
11701− ?. ?=(%generic -.sh) &
11281+::
11703− (module-mold-params-valid vars.sh *(set @t) 256)
11705− =? sh ?=(%generic -.sh) body.sh
11706− ?. ?=(%union -.sh) ~
11707− :: A failed inference keeps no projection, so it is computed once more.
11708− (mold-overlap-witness cases.sh (union-pairs cases.sh molds) molds)
11709−++ module-mold-types-detail
11710− |= [molds=imolds state=istate]
11711− ^- (each imold-types imold-failure)
11713− =/ m=[name=term body=shape] i.molds
11714− =/ t=(unit [template=ischeme state=istate])
11715− (infer-mold-template body.m state(active [name.m active.state], in-mold &))
11717− =/ overlap=(unit upair) (module-mold-overlap m molds.state)
11718− [%| ['module mold needs unsupported inference' ?~(overlap ~ `[name.m u.overlap])]]
11719− =. typ.template.u.t (label-direct-union typ.template.u.t body.m name.m state)
11720− =/ rest=(each imold-types imold-failure) $(molds t.molds)
11721− ?: ?=(%| -.rest) rest
11722− [%& [[name.m template.u.t] p.rest]]
11723++ module-mold-types
11282++ module-mold-types
11724 |= [molds=imolds state=istate]
11283 |= [molds=imolds state=istate]
11725 ^- (each imold-types @t)
11284 ^- (each imold-types @t)
@@ -11777,38 +11336,9 @@
11777 ?. ?=(%tvar -.i.args.tail) |
11336 ?. ?=(%tvar -.i.args.tail) |
11778 =(var name.i.args.tail)
11337 =(var name.i.args.tail)
11780−++ prelude-public-label
11783− ?: =(label 'ask.internal') `'ask'
11784− ?: =(label 'qath.internal') `'qath'
11785− ?: =(label 'raw-poke.internal') `'raw-poke'
11788−++ prelude-label-nested
11793− =/ label=(unit @t) ?~(label.typ ~ (prelude-public-label u.label.typ))
11794− [%union (turn cases.typ |=(c=itype (prelude-label-nested c))) origin.typ label (turn args.typ |=(c=itype (prelude-label-nested c)))]
11796− =/ label=(unit @t) ?~(label.typ ~ (prelude-public-label u.label.typ))
11797− typ(label label, args (turn args.typ |=(c=itype (prelude-label-nested c))))
11799− =/ label=(unit @t) ?~(label.typ ~ (prelude-public-label u.label.typ))
11801− %collection [%collection name.typ (turn args.typ |=(c=itype (prelude-label-nested c)))]
11802− %face [%face name.typ $(typ body.typ)]
11803− %fn [%fn $(typ sample.typ) $(typ product.typ)]
11804− %cell [%cell $(typ hed.typ) $(typ tal.typ)]
11808++ prelude-label
11339++ prelude-label
11809 |= [typ=itype name=term vars=(list @ud)]
11340 |= [typ=itype name=term vars=(list @ud)]
11810 ^- itype
11341 ^- itype
11811− =. typ (prelude-label-nested typ)
11812 ?: ?=(%jrec -.typ) typ(label `name)
11342 ?: ?=(%jrec -.typ) typ(label `name)
11813 ?: ?=(%grec -.typ)
11343 ?: ?=(%grec -.typ)
11814 ?. (identity-union-parameters vars args.typ) typ(label ~)
11344 ?. (identity-union-parameters vars args.typ) typ(label ~)
@@ -11845,14 +11375,7 @@
11845 =/ plus=ischeme [[%fn [%cell b b] b] ~[0]]
11375 =/ plus=ischeme [[%fn [%cell b b] b] ~[0]]
11846 =/ minus=ischeme [[%fn b b] ~[0]]
11376 =/ minus=ischeme [[%fn b b] ~[0]]
11847 =/ greater=ischeme [[%fn pair [%flag ~]] ~[0]]
11377 =/ greater=ischeme [[%fn pair [%flag ~]] ~[0]]
11848− =/ free=itype [%fvar 0]
11849− =/ equal=ischeme [[%fn [%cell free free] [%flag ~]] ~[0]]
11850− =/ utf8=itype [%atom 'tD']
11851− =/ tape=itype [%collection %list ~[utf8]]
11852− =/ codepoints=itype [%collection %list ~[[%atom %c]]]
11853− =/ text-trip=ischeme [[%fn [%atom %t] tape] ~]
11854− =/ text-tuba=ischeme [[%fn tape codepoints] ~]
11855− [~[[%raw-add plus] [%raw-dec minus] [%raw-gth greater] [%raw-eq equal] [%raw-trip text-trip] [%raw-tuba text-tuba]] ~ /lib/jibb/primitives/jibb ~ ~ ~ ~ ~]
11378+ [~[[%raw-add plus] [%raw-dec minus] [%raw-gth greater]] ~ /lib/jibb/primitives/jibb ~ ~ ~ ~ ~]
11857++ infer-private-internal
11380++ infer-private-internal
11858 |= [src=@t public-source=@t]
11381 |= [src=@t public-source=@t]
@@ -12029,74 +11552,6 @@
12029 ?~ (ienv-lookup name.i.ds env) |
11552 ?~ (ienv-lookup name.i.ds env) |
12030 $(ds t.ds)
11553 $(ds t.ds)
12032−:: Names the value a failed full check stops at, for its message only. A
12033−:: value whose module dependencies all resolved failed on its own, so the
12034−:: first such missing value is named. Otherwise every missing value waits
12035−:: on another, so following the first one each waits on, from the first
12036−:: missing value, reaches a value twice, which is named. The walk is over
12037−:: the syntactic dependency graph: dependency-expr ignores binders, so a
12038−:: sample or other local binder with a top-level value's name reads as a
12039−:: dependency on it. The named value is on a cycle of that graph, but may
12040−:: only call into the value that failed, as when a binder in that value
12041−:: shadows the named one. It claims no error in the named value.
12042−++ module-missing-value
12043− |= [ds=(list def) env=ienv]
12045− =/ missing=(list term)
12048− ?. ?=(%value -.d) ~
12049− ?^ (ienv-lookup name.d env) ~
12052− =/ pending=ivisited (graph-nameset missing ~)
12053− =/ roots=(list term)
12056− ?. ?=(%value -.d) ~
12057− ?~ (~(get by pending) name.d) ~
12058− =/ deps=(list term) (dependency-expr val.d)
12059− ?. (levy deps |=(n=term |(=(n name.d) ?=(~ (~(get by pending) n))))) ~
12062− =/ seen=ivisited ~
12063− =/ here=term i.missing
12065− ?^ (~(get by seen) here) `here
12066− =/ next=(list term)
12070− ?. ?=(%value -.d) ~
12071− ?. =(here name.d) ~
12072− (skim (dependency-expr val.d) |=(n=term &(!=(n here) ?=(^ (~(get by pending) n)))))
12074− $(seen (~(put by seen) here &), here i.next)
12076−:: Finds the first missing value that is a gate whose own sample has the
12077−:: name of a value in scope. Partial inference rejects that sample ("sample
12078−:: shadows a name"), and it is an error (grammar, Modules). Mark names name
12079−:: molds and are left out, as are cell samples and binders deeper in the
12081−++ module-sample-shadow
12082− |= [ds=(list def) env=ienv values=(list term)]
12083− ^- (unit [name=term at=span])
12085− ?. ?=(%value -.i.ds) $(ds t.ds)
12086− ?^ (ienv-lookup name.i.ds env) $(ds t.ds)
12087− =/ e=expr val.i.ds
12088− ?. ?=(?(%gate %gate-wide) -.e) $(ds t.ds)
12089− =/ s=sample sample.e
12090− =/ name=(unit term)
12096− ?~ name $(ds t.ds)
12097− ?. (lien values |=(n=term =(n u.name))) $(ds t.ds)
12100:: Cache only completed interfaces for this invocation. The source bundle,
11555:: Cache only completed interfaces for this invocation. The source bundle,
12101:: imported Hoon types and prelude are fixed for the whole graph. Check the
11556:: imported Hoon types and prelude are fixed for the whole graph. Check the
12102:: active path and duplicate sources before consulting it, so a cache hit
11557:: active path and duplicate sources before consulting it, so a cache hit
@@ -12136,25 +11591,6 @@
12136 =(externals.g externals)
11591 =(externals.g externals)
12137 =(marks.g marks)
11592 =(marks.g marks)
12139−++ request-graph-bounded
12140− |= g=irequest-graph
12142− =/ total=@ud (add (lent requests.g) (lent stores.g))
12143− &((lte (lent ~(tap in:..zuse paths.g)) 256) (lte total 256))
12145−++ store-graph-requests-add
12146− |= [pending=(list istore-request-evidence) acc=(list istore-request-evidence) fuel=@ud]
12147− ^- (unit (list istore-request-evidence))
12150− =/ hit=(list istore-request-evidence)
12151− (skim acc |=(x=istore-request-evidence =(store-at.x store-at.i.pending)))
12153− ?. ?=([* ~] hit) ~
12154− ?. =(i.hit i.pending) ~
12155− $(pending t.pending, fuel (dec fuel))
12156− $(pending t.pending, acc [i.pending acc], fuel (dec fuel))
12158++ request-graph-merge
11594++ request-graph-merge
12159 |= [imports=ijimports g=irequest-graph fuel=@ud]
11595 |= [imports=ijimports g=irequest-graph fuel=@ud]
12160 ^- (unit irequest-graph)
11596 ^- (unit irequest-graph)
@@ -12175,13 +11611,8 @@
12175 =/ rs=(unit (list irequest-evidence))
11611 =/ rs=(unit (list irequest-evidence))
12176 (request-graph-requests-add requests.cg requests.g (add 1 (lent requests.cg)))
11612 (request-graph-requests-add requests.cg requests.g (add 1 (lent requests.cg)))
12177 ?~ rs ~
11613 ?~ rs ~
12178− =/ ss=(unit (list istore-request-evidence))
12179− (store-graph-requests-add stores.cg stores.g (add 1 (lent stores.cg)))
12181− =/ total=@ud (add (lent u.rs) (lent u.ss))
12182− ?: &(?=(^ u.rs) |((gth (lent ~(tap in:..zuse merged)) 256) (gth total 256))) ~
11614+ ?: &(?=(^ u.rs) |((gth (lent ~(tap in:..zuse merged)) 256) (gth (lent u.rs) 256))) ~
12183− ?: &(?=(^ u.ss) |((gth (lent ~(tap in:..zuse merged)) 256) (gth total 256))) ~
12184− $(imports t.imports, g g(paths merged, requests u.rs, stores u.ss), fuel (dec fuel))
11615+ $(imports t.imports, g g(paths merged, requests u.rs), fuel (dec fuel))
12185++ request-graph-reusable
11616++ request-graph-reusable
12186 |= [f=ifile src=@t externals=iexternals marks=imark-externals modules=jbundle active=(list path) values=(list term) molds=(list term) prelude=(unit ifile)]
11617 |= [f=ifile src=@t externals=iexternals marks=imark-externals modules=jbundle active=(list path) values=(list term) molds=(list term) prelude=(unit ifile)]
@@ -12196,40 +11627,33 @@
12196++ resolve-jibb-imports
11627++ resolve-jibb-imports
12197 |= [imports=(list import) externals=iexternals mark-externals=imark-externals modules=jbundle active=(list path) prelude-values=(list term) prelude-molds=(list term) cache=jcache prelude=(unit ifile)]
11628 |= [imports=(list import) externals=iexternals mark-externals=imark-externals modules=jbundle active=(list path) prelude-values=(list term) prelude-molds=(list term) cache=jcache prelude=(unit ifile)]
12198 ^- jimports-result
11629 ^- jimports-result
12199− =/ result=jimports-detailed-result
12200− (resolve-jibb-imports-detailed imports externals mark-externals modules active prelude-values prelude-molds cache prelude)
12201− ?: ?=(%| -.result) [%| message.p.result]
12203−++ resolve-jibb-imports-detailed
12204− |= [imports=(list import) externals=iexternals mark-externals=imark-externals modules=jbundle active=(list path) prelude-values=(list term) prelude-molds=(list term) cache=jcache prelude=(unit ifile)]
12205− ^- jimports-detailed-result
12206 ?~ imports [%& [~ cache]]
11630 ?~ imports [%& [~ cache]]
12207 ?. ?=(%jibb -.i.imports) $(imports t.imports)
11631 ?. ?=(%jibb -.i.imports) $(imports t.imports)
12208 =/ at=path (weld path.i.imports `path`~[%jibb])
11632 =/ at=path (weld path.i.imports `path`~[%jibb])
12209 ?: =(at /lib/jibb/internal/jibb)
11633 ?: =(at /lib/jibb/internal/jibb)
12210− [%| ['the prelude internal module is private' ~]]
11634+ [%| 'the prelude internal module is private']
12211 ?: =(at /lib/jibb/primitives/jibb)
11635 ?: =(at /lib/jibb/primitives/jibb)
12212− [%| ['the prelude primitive interface is private' ~]]
11636+ [%| 'the prelude primitive interface is private']
12213 ?: (lien active |=(p=path =(p at)))
11637 ?: (lien active |=(p=path =(p at)))
12214− [%| [(crip "import cycle at {(spud at)}") ~]]
11638+ [%| (crip "import cycle at {(spud at)}")]
12215 =/ found=jbundle (skim modules |=(m=jsource =(at at.m)))
11639 =/ found=jbundle (skim modules |=(m=jsource =(at at.m)))
12216− ?~ found [%| [(crip "module source missing: {(spud at)}") ~]]
11640+ ?~ found [%| (crip "module source missing: {(spud at)}")]
12217− ?^ t.found [%| [(crip "duplicate module sources: {(spud at)}") ~]]
11641+ ?^ t.found [%| (crip "duplicate module sources: {(spud at)}")]
12218 =/ cached=(unit ifile) (find-jibb-cache at cache)
11642 =/ cached=(unit ifile) (find-jibb-cache at cache)
12219− =/ iface=jfile-detailed-result
11643+ =/ iface=jfile-result
12220 ?^ cached
11644 ?^ cached
12221− ?. =(at.u.cached at) [%| ['cached module identity needs unsupported inference' ~]]
11645+ ?. =(at.u.cached at) [%| 'cached module identity needs unsupported inference']
12222 ?~ graph.u.cached
11646 ?~ graph.u.cached
12223 :: A detached legacy interface has unknown evidence. Rebuild it
11647 :: A detached legacy interface has unknown evidence. Rebuild it
12224 :: against the current graph, without retaining any stale entry.
11648 :: against the current graph, without retaining any stale entry.
12225 =/ clean=jcache (skim cache |=(x=[at=path iface=ifile] !=(at.x at)))
11649 =/ clean=jcache (skim cache |=(x=[at=path iface=ifile] !=(at.x at)))
12226− (infer-jibb-file-detailed at source.i.found externals mark-externals modules [at active] prelude-values prelude-molds clean prelude)
11650+ (infer-jibb-file at source.i.found externals mark-externals modules [at active] prelude-values prelude-molds clean prelude)
12227 ?. (request-graph-reusable u.cached source.i.found externals mark-externals modules active prelude-values prelude-molds prelude)
11651 ?. (request-graph-reusable u.cached source.i.found externals mark-externals modules active prelude-values prelude-molds prelude)
12228− [%| ['cached module evidence needs unsupported inference' ~]]
11652+ [%| 'cached module evidence needs unsupported inference']
12229 [%& [u.cached cache]]
11653 [%& [u.cached cache]]
12230− (infer-jibb-file-detailed at source.i.found externals mark-externals modules [at active] prelude-values prelude-molds cache prelude)
11654+ (infer-jibb-file at source.i.found externals mark-externals modules [at active] prelude-values prelude-molds cache prelude)
12231 ?: ?=(%| -.iface) [%| p.iface]
11655 ?: ?=(%| -.iface) [%| p.iface]
12232− =/ rest=jimports-detailed-result $(imports t.imports, cache cache.p.iface)
11656+ =/ rest=jimports-result $(imports t.imports, cache cache.p.iface)
12233 ?: ?=(%| -.rest) rest
11657 ?: ?=(%| -.rest) rest
12234 [%& [[[face.i.imports iface.p.iface] resolved.p.rest] cache.p.rest]]
11658 [%& [[[face.i.imports iface.p.iface] resolved.p.rest] cache.p.rest]]
@@ -12367,66 +11791,27 @@
12367 =/ outer=(list term) (weld prelude-values (weld (global-value-names defs.mod) (api-import-faces imports.mod)))
11791 =/ outer=(list term) (weld prelude-values (weld (global-value-names defs.mod) (api-import-faces imports.mod)))
12368 (levy derived |=(n=term &((unique-value-name n derived) !(lien outer |=(x=term =(n x))))))
11792 (levy derived |=(n=term &((unique-value-name n derived) !(lien outer |=(x=term =(n x))))))
12370−:: The definite error behind some failures of the check above. An API
12371−:: exports `poke` when it declares `+$ poke`, and a request per case of a
12372−:: `+$ paths` that reads as path cases; these names surely exist, so a clash
12373−:: among them or with the module's scope is an error (grammar, Modules). A
12374−:: reserved `proj` stays unsupported, as in the check above.
12375−++ api-derived-clash
12376− |= [mod=module prelude-values=(list term)]
12378− =/ declared=(list term) (collect-mark-imports imports.mod)
12379− =/ declarations=(list def)
12380− (skim defs.mod |=(d=def &(?=(%mold -.d) =(%paths name.d))))
12381− =/ cases=(list [name=term at=span note=tape])
12382− ?. ?=([* ~] declarations) ~
12383− =/ decl=def i.declarations
12384− ?> ?=(%mold -.decl)
12385− =/ paths=(unit (list iapi-path)) (api-path-declaration shape.decl declared)
12387− (turn u.paths |=(p=iapi-path [name.p at.p "`{(trip name.p)}` is derived from this path case"]))
12388− =/ pokes=(list def)
12389− (skim defs.mod |=(d=def &(?=(%mold -.d) =(%poke name.d))))
12390− =/ derived=(list [name=term at=span note=tape])
12391− ?. ?=([* ~] pokes) cases
12392− (snoc cases [%poke at.i.pokes "`poke` is derived from this mold"])
12393− =/ names=(list term) (turn derived |=(x=[name=term at=span note=tape] name.x))
12394− =/ outer=(list term) (weld prelude-values (weld (global-value-names defs.mod) (api-import-faces imports.mod)))
12395− =/ clashes=(list term)
12399− &((unique-value-name n names) !(lien outer |=(x=term =(n x))))
12402− =/ sites=(list [at=span note=tape])
12404− |= x=[name=term at=span note=tape]
12405− ?. =(i.clashes name.x) ~
12407− `(derived-name-clash "API" i.clashes sites mod)
12409:: Analysis only. Successful external entries must be unchanged results
11794:: Analysis only. Successful external entries must be unchanged results
12410:: produced for the declared marks; no request interface is produced.
11795:: produced for the declared marks; no request interface is produced.
12411+$ iapi-mark-type [name=term typ=itype]
11796+$ iapi-mark-type [name=term typ=itype]
12412+$ iapi-path-typed [path=iapi-path full=itype diffs=(list iapi-mark-type)]
11797+$ iapi-path-typed [path=iapi-path full=itype diffs=(list iapi-mark-type)]
12413++ api-diff-types
11798++ api-diff-types
12414− |= [names=(list term) externals=imark-externals declared=(list term) prelude=ifile]
11799+ |= [names=(list term) externals=imark-externals declared=(list term)]
12415 ^- (unit (list iapi-mark-type))
11800 ^- (unit (list iapi-mark-type))
12416 ?~ names `~
11801 ?~ names `~
12417− =/ typ=(unit itype) (find-imported-mark-prelude i.names externals declared prelude)
11802+ =/ typ=(unit itype) (find-imported-mark i.names externals declared)
12418 ?~ typ ~
11803 ?~ typ ~
12419 =/ tail=(unit (list iapi-mark-type)) $(names t.names)
11804 =/ tail=(unit (list iapi-mark-type)) $(names t.names)
12420 ?~ tail ~
11805 ?~ tail ~
12421 `[[i.names u.typ] u.tail]
11806 `[[i.names u.typ] u.tail]
12423++ api-path-types
11808++ api-path-types
12424− |= [paths=(list iapi-path) externals=imark-externals declared=(list term) prelude=ifile]
11809+ |= [paths=(list iapi-path) externals=imark-externals declared=(list term)]
12425 ^- (unit (list iapi-path-typed))
11810 ^- (unit (list iapi-path-typed))
12426 ?~ paths `~
11811 ?~ paths `~
12427− =/ full=(unit itype) (find-imported-mark-prelude full.i.paths externals declared prelude)
11812+ =/ full=(unit itype) (find-imported-mark full.i.paths externals declared)
12428 ?~ full ~
11813 ?~ full ~
12429− =/ diffs=(unit (list iapi-mark-type)) (api-diff-types diffs.i.paths externals declared prelude)
11814+ =/ diffs=(unit (list iapi-mark-type)) (api-diff-types diffs.i.paths externals declared)
12430 ?~ diffs ~
11815 ?~ diffs ~
12431 =/ tail=(unit (list iapi-path-typed)) $(paths t.paths)
11816 =/ tail=(unit (list iapi-path-typed)) $(paths t.paths)
12432 ?~ tail ~
11817 ?~ tail ~
@@ -12446,7 +11831,7 @@
12446 `~[u.name]
11831 `~[u.name]
12448++ api-path-analysis
11833++ api-path-analysis
12449− |= [mod=module externals=imark-externals prelude-values=(list term) prelude-molds=(list term) prelude=ifile]
11834+ |= [mod=module externals=imark-externals prelude-values=(list term) prelude-molds=(list term)]
12450 ^- (unit (list iapi-path-typed))
11835 ^- (unit (list iapi-path-typed))
12451 ?: (lien defs.mod def-has-hole) ~
11836 ?: (lien defs.mod def-has-hole) ~
12452 ?^ (duplicate-defs defs.mod) ~
11837 ?^ (duplicate-defs defs.mod) ~
@@ -12467,9 +11852,8 @@
12467 ?> ?=(%mold -.decl)
11852 ?> ?=(%mold -.decl)
12468 =/ paths=(unit (list iapi-path)) (api-path-declaration shape.decl declared)
11853 =/ paths=(unit (list iapi-path)) (api-path-declaration shape.decl declared)
12469 ?~ paths ~
11854 ?~ paths ~
12470− =/ derived-pokes=(list term) ?~(pokes ~ ~[%poke])
12471− ?. (api-derived-names-valid u.paths derived-pokes mod prelude-values) ~
11855+ ?. (api-derived-names-valid u.paths u.poke-names mod prelude-values) ~
12472− (api-path-types u.paths externals declared prelude)
11856+ (api-path-types u.paths externals declared)
12474:: Source/graph entry for path analysis only. The returned paths retain
11858:: Source/graph entry for path analysis only. The returned paths retain
12475:: reader-derived mark types and import resolution has checked reachable
11859:: reader-derived mark types and import resolution has checked reachable
@@ -12483,16 +11867,12 @@
12483 =/ duplicate=(unit idiag) (duplicate-defs defs.p.parsed)
11867 =/ duplicate=(unit idiag) (duplicate-defs defs.p.parsed)
12484 ?^ duplicate [%| (show-duplicate-fields file src u.duplicate)]
11868 ?^ duplicate [%| (show-duplicate-fields file src u.duplicate)]
12485 ?~ prepared [%| 'API path analysis needs the prepared prelude']
11869 ?~ prepared [%| 'API path analysis needs the prepared prelude']
12486− =/ public=ifile iface.u.prepared
12487− :: The analysis below would call a derived-name clash unsupported.
12488− =/ clash=(unit idiag) (api-derived-clash p.parsed values.u.prepared)
12489− ?^ clash [%| (show-duplicate-fields file src u.clash)]
12490 =/ prelude=(unit ifile) `iface.u.prepared
11870 =/ prelude=(unit ifile) `iface.u.prepared
12491 =/ deps=jimports-result
11871 =/ deps=jimports-result
12492 (resolve-jibb-imports imports.p.parsed externals marks modules ~[file] values.u.prepared molds.u.prepared ~ prelude)
11872 (resolve-jibb-imports imports.p.parsed externals marks modules ~[file] values.u.prepared molds.u.prepared ~ prelude)
12493 ?: ?=(%| -.deps) [%| p.deps]
11873 ?: ?=(%| -.deps) [%| p.deps]
12494 =/ paths=(unit (list iapi-path-typed))
11874 =/ paths=(unit (list iapi-path-typed))
12495− (api-path-analysis p.parsed marks values.u.prepared molds.u.prepared public)
11875+ (api-path-analysis p.parsed marks values.u.prepared molds.u.prepared)
12496 ?~ paths [%| 'API path declaration needs unsupported analysis']
11876 ?~ paths [%| 'API path declaration needs unsupported analysis']
12497 [%& u.paths]
11877 [%& u.paths]
@@ -12512,15 +11892,12 @@
12512 =/ duplicate=(unit idiag) (duplicate-defs defs.p.parsed)
11892 =/ duplicate=(unit idiag) (duplicate-defs defs.p.parsed)
12513 ?^ duplicate [%| (show-duplicate-fields file src u.duplicate)]
11893 ?^ duplicate [%| (show-duplicate-fields file src u.duplicate)]
12514 ?~ prepared [%| 'API path evidence needs the prepared prelude']
11894 ?~ prepared [%| 'API path evidence needs the prepared prelude']
12515− :: The analysis below would call a derived-name clash unsupported.
12516− =/ clash=(unit idiag) (api-derived-clash p.parsed values.u.prepared)
12517− ?^ clash [%| (show-duplicate-fields file src u.clash)]
12518 =/ public=ifile iface.u.prepared
11895 =/ public=ifile iface.u.prepared
12519 =/ deps=jimports-result
11896 =/ deps=jimports-result
12520 (resolve-jibb-imports imports.p.parsed externals marks modules ~[file] values.u.prepared molds.u.prepared ~ `public)
11897 (resolve-jibb-imports imports.p.parsed externals marks modules ~[file] values.u.prepared molds.u.prepared ~ `public)
12521 ?: ?=(%| -.deps) [%| p.deps]
11898 ?: ?=(%| -.deps) [%| p.deps]
12522 =/ paths=(unit (list iapi-path-typed))
11899 =/ paths=(unit (list iapi-path-typed))
12523− (api-path-analysis p.parsed marks values.u.prepared molds.u.prepared public)
11900+ (api-path-analysis p.parsed marks values.u.prepared molds.u.prepared)
12524 ?~ paths [%| 'API path declaration needs unsupported analysis']
11901 ?~ paths [%| 'API path declaration needs unsupported analysis']
12525 [%& [file src u.prepared externals marks cache.p.deps u.paths]]
11902 [%& [file src u.prepared externals marks cache.p.deps u.paths]]
12526:: Graph-aware variant preserves the caller active stack and cache.
11903:: Graph-aware variant preserves the caller active stack and cache.
@@ -12536,15 +11913,12 @@
12536 =/ duplicate=(unit idiag) (duplicate-defs defs.p.parsed)
11913 =/ duplicate=(unit idiag) (duplicate-defs defs.p.parsed)
12537 ?^ duplicate [%| (show-duplicate-fields file src u.duplicate)]
11914 ?^ duplicate [%| (show-duplicate-fields file src u.duplicate)]
12538 ?~ prepared [%| 'API path evidence needs the prepared prelude']
11915 ?~ prepared [%| 'API path evidence needs the prepared prelude']
12539− :: The analysis below would call a derived-name clash unsupported.
12540− =/ clash=(unit idiag) (api-derived-clash p.parsed values.u.prepared)
12541− ?^ clash [%| (show-duplicate-fields file src u.clash)]
12542 =/ public=ifile iface.u.prepared
11916 =/ public=ifile iface.u.prepared
12543 =/ deps=jimports-result
11917 =/ deps=jimports-result
12544 (resolve-jibb-imports imports.p.parsed externals marks modules active values.u.prepared molds.u.prepared cache `public)
11918 (resolve-jibb-imports imports.p.parsed externals marks modules active values.u.prepared molds.u.prepared cache `public)
12545 ?: ?=(%| -.deps) [%| p.deps]
11919 ?: ?=(%| -.deps) [%| p.deps]
12546 =/ paths=(unit (list iapi-path-typed))
11920 =/ paths=(unit (list iapi-path-typed))
12547− (api-path-analysis p.parsed marks values.u.prepared molds.u.prepared public)
11921+ (api-path-analysis p.parsed marks values.u.prepared molds.u.prepared)
12548 ?~ paths [%| 'API path declaration needs unsupported analysis']
11922 ?~ paths [%| 'API path declaration needs unsupported analysis']
12549 [%& [file src u.prepared externals marks cache.p.deps u.paths]]
11923 [%& [file src u.prepared externals marks cache.p.deps u.paths]]
@@ -12631,7 +12005,7 @@
12631 =/ vals=(list term) (global-value-names ordinary)
12005 =/ vals=(list term) (global-value-names ordinary)
12632 ?: (lien vals |=(n=term =(n %main))) [%| 'API module kind needs unsupported inference']
12006 ?: (lien vals |=(n=term =(n %main))) [%| 'API module kind needs unsupported inference']
12633 =/ declared=(list term) (collect-mark-imports imports.mod)
12007 =/ declared=(list term) (collect-mark-imports imports.mod)
12634− =/ mark-types=(unit (list iapi-mark-type)) (api-diff-types declared marks declared iface.prep)
12008+ =/ mark-types=(unit (list iapi-mark-type)) (api-diff-types declared marks declared)
12635 ?~ mark-types [%| 'API declared marks need unsupported inference']
12009 ?~ mark-types [%| 'API declared marks need unsupported inference']
12636 =/ prelude=(unit ifile) `iface.prep
12010 =/ prelude=(unit ifile) `iface.prep
12637 =/ deps=jimports-result
12011 =/ deps=jimports-result
@@ -12665,7 +12039,7 @@
12665 =/ vals=(list term) (global-value-names ordinary)
12039 =/ vals=(list term) (global-value-names ordinary)
12666 ?: (lien vals |=(n=term =(n %main))) [%| 'API module kind needs unsupported inference']
12040 ?: (lien vals |=(n=term =(n %main))) [%| 'API module kind needs unsupported inference']
12667 =/ declared=(list term) (collect-mark-imports imports.mod)
12041 =/ declared=(list term) (collect-mark-imports imports.mod)
12668− =/ mark-types=(unit (list iapi-mark-type)) (api-diff-types declared marks declared iface.prep)
12042+ =/ mark-types=(unit (list iapi-mark-type)) (api-diff-types declared marks declared)
12669 ?~ mark-types [%| 'API declared marks need unsupported inference']
12043 ?~ mark-types [%| 'API declared marks need unsupported inference']
12670 =/ prelude=(unit ifile) `iface.prep
12044 =/ prelude=(unit ifile) `iface.prep
12671 =/ deps=jimports-result
12045 =/ deps=jimports-result
@@ -12689,29 +12063,6 @@
12689:: Value watchability remains unproved even for a watchable declaration.
12063:: Value watchability remains unproved even for a watchable declaration.
12690+$ ione-request-interface
12064+$ ione-request-interface
12691 [support=iapi-support-evidence parts=iapi-request-parts iface=ifile]
12065 [support=iapi-support-evidence parts=iapi-request-parts iface=ifile]
12692−++ compatible-raw-poke
12693− |= prelude=iprelude
12695− =/ public=ifile iface.prelude
12696− ?. =(at.public /lib/jibb/prelude/jibb) ~
12697− =/ poke=(unit ischeme) (find-jibb-mold %raw-poke public)
12700− ?. ?=(%union -.typ.u.poke) ~
12701− ?^ args.typ.u.poke ~
12702− ?. =(origin.typ.u.poke `[/lib/jibb/internal/jibb %raw-poke]) ~
12703− ?: (itype-has-tag typ.u.poke) ~
12704− =/ private=(list iwidth-dependency)
12705− (skim dependencies.public |=(d=iwidth-dependency =(at.d /lib/jibb/internal/jibb)))
12706− ?. ?=([* ~] private) ~
12707− ?~ source.i.private ~
12708− =/ agent-case=itype
12709− [%cell [%const [%term %tas %agent '%agent']] [%cell [%face %agent [%atom %tas]] [%cell [%face %mark [%atom %tas]] [%face %payload [%noun ~]]]]]
12710− =/ store-case=itype
12711− [%cell [%const [%term %tas %store '%store']] [%cell [%face %module [%atom %t]] [%cell [%face %action [%atom %tas]] [%face %payload [%noun ~]]]]]
12712− ?. =(cases.typ.u.poke ~[agent-case store-case]) ~
12715++ request-compatible-ask
12066++ request-compatible-ask
12716 |= prelude=iprelude
12067 |= prelude=iprelude
12717 ^- (unit ischeme)
12068 ^- (unit ischeme)
@@ -12808,7 +12159,7 @@
12808 ?~ source.i.private [%| 'request internal source needs unsupported inference']
12159 ?~ source.i.private [%| 'request internal source needs unsupported inference']
12809 =/ req=irequest-evidence
12160 =/ req=irequest-evidence
12810 [file name.path.p p src u.source.public u.source.i.private values.prelude molds.prelude externals marks]
12161 [file name.path.p p src u.source.public u.source.i.private values.prelude molds.prelude externals marks]
12811− =/ interface=ifile [~[[name.path.p scheme]] exports file ~ ~ ~ `src `[(silt `(list path)`~[file]) ~[req] ~ modules `public values.prelude molds.prelude externals marks]]
12162+ =/ interface=ifile [~[[name.path.p scheme]] exports file ~ ~ ~ `src `[(silt `(list path)`~[file]) ~[req] modules `public values.prelude molds.prelude externals marks]]
12812 [%& [support u.parts interface]]
12163 [%& [support u.parts interface]]
12813:: Graph-aware request artifact; resolver use remains type-only.
12164:: Graph-aware request artifact; resolver use remains type-only.
12814++ one-request-interface-graph
12165++ one-request-interface-graph
@@ -12862,14 +12213,14 @@
12862 ?~ source.i.private [%| 'request internal source needs unsupported inference']
12213 ?~ source.i.private [%| 'request internal source needs unsupported inference']
12863 =/ req=irequest-evidence
12214 =/ req=irequest-evidence
12864 [file name.path.p p src u.source.public u.source.i.private values.prelude molds.prelude externals marks]
12215 [file name.path.p p src u.source.public u.source.i.private values.prelude molds.prelude externals marks]
12865− =/ interface=ifile [~[[name.path.p scheme]] exports file ~ ~ ~ `src `[(silt `(list path)`~[file]) ~[req] ~ modules `public values.prelude molds.prelude externals marks]]
12216+ =/ interface=ifile [~[[name.path.p scheme]] exports file ~ ~ ~ `src `[(silt `(list path)`~[file]) ~[req] modules `public values.prelude molds.prelude externals marks]]
12866 [%& [support u.parts interface]]
12217 [%& [support u.parts interface]]
12868++ api-mark-exports
12219++ api-mark-exports
12869− |= [marks=(list term) all=(list term) externals=imark-externals prelude=ifile]
12220+ |= [marks=(list term) all=(list term) externals=imark-externals]
12870 ^- imold-types
12221 ^- imold-types
12871 ?~ marks ~
12222 ?~ marks ~
12872− =/ t=(unit itype) (find-imported-mark-prelude i.marks externals all prelude)
12223+ =/ t=(unit itype) (find-imported-mark i.marks externals all)
12873 ?~ t $(marks t.marks)
12224 ?~ t $(marks t.marks)
12874 [[i.marks [u.t ~]] $(marks t.marks)]
12225 [[i.marks [u.t ~]] $(marks t.marks)]
@@ -12878,54 +12229,37 @@
12878++ api-poke-interface
12229++ api-poke-interface
12879 |= [at=path mod=module mark-externals=imark-externals prelude-values=(list term) prelude-molds=(list term) prelude=(unit ifile)]
12230 |= [at=path mod=module mark-externals=imark-externals prelude-values=(list term) prelude-molds=(list term) prelude=(unit ifile)]
12880 ^- (unit ifile)
12231 ^- (unit ifile)
12881− =/ out=(each ifile @t)
12882− (api-poke-interface-result at mod mark-externals prelude-values prelude-molds prelude)
12883− ?:(?=(%& -.out) `p.out ~)
12885−:: The same check, naming the part that stopped it. Each reason says which
12886−:: part is outside this fragment and claims no error in the module, except
12887−:: duplicate definitions, an error the full check reports first, as for
12889−++ api-poke-interface-result
12890− |= [at=path mod=module mark-externals=imark-externals prelude-values=(list term) prelude-molds=(list term) prelude=(unit ifile)]
12891− ^- (each ifile @t)
12892− ?: (lien defs.mod def-has-hole) [%| 'API holes need unsupported inference']
12232+ ?: (lien defs.mod def-has-hole) ~
12893− ?. ?=([%ui %api @ %jibb ~] at) [%| 'API path evidence requires /ui/api/<agent>.jibb']
12233+ ?. ?=([%ui %api @ %jibb ~] at) ~
12894− ?^ (duplicate-defs defs.mod) [%| 'API has duplicate definitions']
12234+ ?^ (duplicate-defs defs.mod) ~
12895− ?~ prelude [%| 'API poke prelude needs unsupported inference']
12235+ ?~ prelude ~
12896− ?. =(at.u.prelude /lib/jibb/prelude/jibb) [%| 'API poke prelude needs unsupported inference']
12236+ ?. =(at.u.prelude /lib/jibb/prelude/jibb) ~
12897− =/ poke=(unit ischeme) (find-jibb-mold %raw-poke u.prelude)
12237+ =/ poke=(unit ischeme) (find-jibb-mold %poke u.prelude)
12898− ?~ poke [%| 'API poke prelude needs unsupported inference']
12238+ ?~ poke ~
12899− ?. ?=(%union -.typ.u.poke) [%| 'API poke prelude needs unsupported inference']
12239+ ?. ?=(%union -.typ.u.poke) ~
12900− ?^ vars.u.poke [%| 'API poke prelude needs unsupported inference']
12240+ ?^ vars.u.poke ~
12901 =/ compatible=?
12241 =/ compatible=?
12902 %+ lien cases.typ.u.poke
12242 %+ lien cases.typ.u.poke
12903 |= c=itype
12243 |= c=itype
12904 ?=([%cell [%const [%term %tas %agent *]] [%cell [%face %agent [%atom %tas]] [%cell [%face %mark [%atom %tas]] [%face %payload [%noun ~]]]]] c)
12244 ?=([%cell [%const [%term %tas %agent *]] [%cell [%face %agent [%atom %tas]] [%cell [%face %mark [%atom %tas]] [%face %payload [%noun ~]]]]] c)
12905− ?. compatible [%| 'API poke prelude needs unsupported inference']
12245+ ?. compatible ~
12906− :: Definitions come before imports so that a module with more than a
12907− :: `+$ poke` is not described by its imports.
12908− =/ ds=(list def) defs.mod
12909− ?. ?=([[%mold *] ~] ds) [%| 'poke-only API definitions need unsupported inference']
12910− ?. =(%poke name.i.ds) [%| 'poke-only API definitions need unsupported inference']
12911− ?. (module-scope-valid mod(defs ~) prelude-values prelude-molds) [%| 'API import scope needs unsupported inference']
12246+ ?. (module-scope-valid mod(defs ~) prelude-values prelude-molds) ~
12912− ?. (levy imports.mod |=(i=import ?=(%mark -.i))) [%| 'poke-only API imports need unsupported inference']
12247+ ?. (levy imports.mod |=(i=import ?=(%mark -.i))) ~
12913 =/ marks=(list term) (collect-mark-imports imports.mod)
12248 =/ marks=(list term) (collect-mark-imports imports.mod)
12914− ?. ?=([@ ~] marks) [%| 'poke-only API mark imports need unsupported inference']
12249+ ?. ?=([@ ~] marks) ~
12250+ =/ ds=(list def) defs.mod
12251+ ?. ?=([[%mold *] ~] ds) ~
12252+ ?. =(%poke name.i.ds) ~
12915 =/ sh=shape shape.i.ds
12253 =/ sh=shape shape.i.ds
12916− ?. ?=([%ref *] sh) [%| 'API poke mold needs unsupported inference']
12254+ ?. ?=([%ref *] sh) ~
12917− ?. ?=([@ ~] names.sh) [%| 'API poke mold needs unsupported inference']
12255+ ?. ?=([@ ~] names.sh) ~
12918 =/ n=term i.names.sh
12256 =/ n=term i.names.sh
12919− ?. (unique-value-name n marks) [%| 'API poke mold needs unsupported inference']
12257+ ?. (unique-value-name n marks) ~
12920− ?: |((lien prelude-values |=(x=term =(n x))) (lien prelude-molds |=(x=term =(n x)))) [%| 'API poke mold needs unsupported inference']
12258+ ?: |((lien prelude-values |=(x=term =(n x))) (lien prelude-molds |=(x=term =(n x)))) ~
12921− =/ results=@ud (lent (skim mark-externals |=(e=[mark=term result=*] =(n mark.e))))
12922− ?: =(0 results) [%| (crip "API poke mark %{(trip n)} has no reader result")]
12923− ?. =(1 results) [%| (crip "API poke mark %{(trip n)} has duplicate reader results")]
12924− =/ mark=(unit itype) (find-imported-mark-prelude n mark-externals marks u.prelude)
12259+ =/ mark=(unit itype) (find-imported-mark n mark-externals marks)
12925− ?~ mark [%| 'API poke mark reader result needs unsupported inference']
12260+ ?~ mark ~
12926− =/ sc=(unit ischeme) (derived-poke-command-scheme u.prelude u.mark)
12261+ =/ sc=ischeme [[%fn u.mark typ.u.poke] ~]
12927− ?~ sc [%| 'API poke command needs unsupported inference']
12928− [%& [~[[%poke u.sc]] (api-mark-exports marks marks mark-externals u.prelude) at ~[[n i.t.t.at n]] ~ ~ ~ ~]]
12262+ `[~[[n sc]] (api-mark-exports marks marks mark-externals) at ~[[n i.t.t.at n]] ~ ~ ~ ~]
12930:: Source-proven ordinary helpers validate each selected /sur dependency.
12264:: Source-proven ordinary helpers validate each selected /sur dependency.
12931:: Unused or less direct cores remain unsupported by this first interface.
12265:: Unused or less direct cores remain unsupported by this first interface.
@@ -13048,1624 +12382,26 @@
13048 [%| 'API exported molds need unsupported inference']
12382 [%| 'API exported molds need unsupported inference']
13049 =/ env=ienv (weld values.u.gates (weld values.u.poke values.support))
12383 =/ env=ienv (weld values.u.gates (weld values.u.poke values.support))
13050 =/ graph=irequest-graph
12384 =/ graph=irequest-graph
13051− [(silt `(list path)`~[file]) requests.u.gates ~ modules `public values.prep molds.prep externals marks]
12385+ [(silt `(list path)`~[file]) requests.u.gates modules `public values.prep molds.prep externals marks]
13052 =/ iface=ifile
12386 =/ iface=ifile
13053 [env exports file derived.u.poke elaborations.support ~ `src `graph]
12387 [env exports file derived.u.poke elaborations.support ~ `src `graph]
13054 [%& [iface dependencies.ev]]
12388 [%& [iface dependencies.ev]]
13056−:: A checked program main is only the direct four-component source call.
13057−:: Grouping is transparent, but aliases, qualified wings and other module
13058−:: kinds remain outside this slice.
13059−++ program-main-def
13063− ?: &(?=(%value -.i.ds) =(%main name.i.ds)) `i.ds
13066−++ program-main-wing
13069− ?: ?=(%group -.e) $(e inner.e)
13070− ?. ?=(%wing -.e) ~
13071− ?. ?=([@ ~] names.e) ~
13074−++ program-main-args
13076− ^- (unit (list expr))
13077− ?. ?=(%value -.d) ~
13079− ?: ?=(%group -.val.d) $(val.d inner.val.d)
13080− ?. ?=(%call -.val.d) ~
13081− =/ head=(unit term) (program-main-wing head.val.d)
13083− ?. =(%program u.head) ~
13084− ?. ?=([* * * * ~] args.val.d) ~
13087−++ program-main-parts
13089− ^- (unit [init=term update=term view=term subs=term])
13090− ?. ?=(%value -.d) ~
13092− ?: ?=(%group -.val.d) $(val.d inner.val.d)
13093− ?. ?=(%call -.val.d) ~
13094− =/ head=(unit term) (program-main-wing head.val.d)
13096− ?. =(%program u.head) ~
13097− ?. ?=([* * * * ~] args.val.d) ~
13098− =/ args=(list expr) args.val.d
13099− ?> ?=([* * * * ~] args)
13100− =/ init=(unit term) (program-main-wing i.args)
13101− =/ update=(unit term) (program-main-wing i.t.args)
13102− =/ view=(unit term) (program-main-wing i.t.t.args)
13103− =/ subs=(unit term) (program-main-wing i.t.t.t.args)
13108− `[u.init u.update u.view u.subs]
13110−:: A data page is only the direct two-component source call. Grouping is
13111−:: transparent, but page aliases, qualified wings and other kinds are not.
13114− ^- (unit [load=term view=term])
13115− ?. ?=(%value -.d) ~
13117− ?: ?=(%group -.val.d) $(val.d inner.val.d)
13118− ?. ?=(%call -.val.d) ~
13119− =/ head=(unit term) (program-main-wing head.val.d)
13121− ?. =(%page u.head) ~
13122− ?. ?=([* * ~] args.val.d) ~
13123− =/ args=(list expr) args.val.d
13124− ?> ?=([* * ~] args)
13125− =/ load=(unit term) (program-main-wing i.args)
13126− =/ view=(unit term) (program-main-wing i.t.args)
13131−:: A store main is only the direct two-wing source call. Its local poke mold
13132−:: is checked here and remains in ordinary mold/value inference.
13133−++ store-main-parts
13135− ^- (unit [init=term update=term])
13136− ?. ?=(%value -.d) ~
13138− ?: ?=(%group -.val.d) $(val.d inner.val.d)
13139− ?. ?=(%call -.val.d) ~
13140− =/ head=(unit term) (program-main-wing head.val.d)
13142− ?. =(%store u.head) ~
13143− ?. ?=([* * ~] args.val.d) ~
13144− =/ args=(list expr) args.val.d
13145− ?> ?=([* * ~] args)
13146− =/ init=(unit term) (program-main-wing i.args)
13147− =/ update=(unit term) (program-main-wing i.t.args)
13150− `[u.init u.update]
13152−+$ istore-declaration [action=term defs=(list def)]
13153−:: A failure carries a diagnostic only when it is a definite error of the
13154−:: source; every other failure is unsupported and carries none.
13155−++ store-declaration
13156− |= [mod=module prelude-values=(list term) prelude-molds=(list term)]
13157− ^- (each istore-declaration (unit idiag))
13158− =/ ds=(list def) defs.mod
13159− =/ pokes=(list def)
13160− (skim ds |=(d=def &(?=(%mold -.d) =(%poke name.d))))
13161− ?. ?=([* ~] pokes) [%| ~]
13162− =/ states=(list def)
13163− (skim ds |=(d=def &(?=(%mold -.d) =(%state name.d))))
13164− ?. ?=([* ~] states) [%| ~]
13165− =/ poke=def i.pokes
13166− =/ state=def i.states
13167− ?> &(?=(%mold -.poke) ?=(%mold -.state))
13168− ?: ?=(%generic -.shape.state) [%| ~]
13169− ?: ?=(%generic -.shape.poke) [%| ~]
13170− =/ action=term %poke
13171− =/ ordinary=(list def) ds
13172− =/ derived=(list term) ~[%state action]
13173− ?: (lien derived |=(n=term =(n %proj))) [%| ~]
13174− =/ outer=(list term)
13175− (weld prelude-values (weld (global-value-names ordinary) (api-import-faces imports.mod)))
13176− =/ clashes=(list term)
13177− (skip derived |=(n=term &((unique-value-name n derived) !(lien outer |=(x=term =(n x))))))
13178− :: main's `store` is the prelude's builder when the prelude declares it and
13179− :: nothing local takes the name. Only then do the derived names surely
13180− :: exist, and then a clash is an error even where the scope also fails, as
13181− :: for an import face that clashes with both a derived name and its mold.
13183− ?& (lien prelude-values |=(x=term =(x %store)))
13184− !(lien (global-value-names ds) |=(x=term =(x %store)))
13185− !(lien (import-binding-names imports.mod) |=(x=term =(x %store)))
13187− ?: &(?=(^ clashes) builder (lien outer |=(x=term =(x i.clashes))))
13188− =/ from=span ?:(=(%state i.clashes) at.state at.poke)
13189− =/ derived=[at=span note=tape] [from "`{(trip i.clashes)}` is derived from this mold"]
13190− [%| `(derived-name-clash "store" i.clashes ~[derived] mod)]
13191− ?. (module-scope-valid mod prelude-values prelude-molds) [%| ~]
13193− [%& [action ordinary]]
13195−:: A store or API exports names derived from its declarations, and a
13196−:: clashing derived name is an error (grammar, Modules). Show where the name
13197−:: is derived and the definition, import face or other derived name it
13198−:: clashes with; a prelude name has no site in the module.
13199−++ derived-name-clash
13200− |= [kind=tape n=term derived=(list [at=span note=tape]) mod=module]
13202− =/ values=(list span)
13203− (murn defs.mod |=(d=def ?.(&(?=(%value -.d) =(n name.d)) ~ `at.d)))
13204− =/ faces=(list span)
13205− %+ murn imports.mod
13209− %sur ?.(=(n name.i) ~ `at.i)
13210− %jibb ?.(=(n face.i) ~ `at.i)
13212− =/ head=tape "{kind} derived name `{(trip n)}` clashes with"
13214− ["{head} a definition" (weld derived ~[[i.values "clashing definition"]])]
13216− ["{head} an import face" (weld derived ~[[i.faces "clashing import face"]])]
13217− ?: ?=([* * *] derived)
13218− ["{head} another derived name" derived]
13219− ["{head} a prelude name" derived]
13221−++ program-empty-null
13225− %lit =(%null form.lit.e)
13227− %group $(e inner.e)
13228− %body ?~(defs.e $(e final.e) |)
13232−++ program-subs-empty
13235− ?. ?=(%value -.d) |
13237− %gate (program-empty-null body.val.d)
13238− %gate-wide (program-empty-null body.val.d)
13242−++ program-transparent
13246− %group $(e inner.e)
13248− %body ?~(defs.e $(e final.e) e)
13251−++ program-init-tuple-null
13254− ?. ?=(%value -.d) |
13255− ?. |(?=(%gate -.val.d) ?=(%gate-wide -.val.d)) |
13259− %gate-wide body.val.d
13262− =. body (program-transparent body)
13263− ?. ?=(%tuple -.body) |
13265− (program-empty-null val:(rear items.body))
13267−:: Recover only the update of an already recognized direct program main.
13268−:: Its written sample determines the message/model relationship; the canonical
13269−:: cmd, unit and update slot determine the result context. Publication is
13270−:: component-local so later subscription/view/initializer retries can accumulate.
13271−++ program-update-context
13272− |= [main=def parts=[init=term update=term view=term subs=term] ds=(list def) resolution=iresolved initial=istate]
13273− ^- (unit iresolved)
13274− =/ env=ienv env.resolution
13275− ?^ (ienv-lookup %main env) ~
13276− ?^ (ienv-lookup update.parts env) ~
13277− =/ updates=(list def)
13278− (skim ds |=(d=def &(?=(%value -.d) =(update.parts name.d))))
13279− ?. ?=([* ~] updates) ~
13280− =/ update-def=def i.updates
13281− ?> ?=(%value -.update-def)
13282− =/ written-update=(unit sample) (direct-gate-sample update-def)
13283− ?~ written-update ~
13284− ?. ?=(%cell -.u.written-update) ~
13285− ?. ?=([* * ~] items.u.written-update) ~
13286− ?~ prelude.initial ~
13287− =/ program=(unit ischeme) (ienv-lookup %program values.u.prelude.initial)
13289− =/ command=(unit ischeme) (find-jibb-mold %cmd u.prelude.initial)
13290− =/ list-template=(unit ischeme) (find-jibb-mold %list u.prelude.initial)
13292− ?~ list-template ~
13293− =/ heads=(unit igate-prelude-evidence) (direct-prelude-evidence ds prelude.initial)
13295− =/ written=(unit def) (~(get by gates.u.heads) %program)
13297− =/ written-sample=(unit sample) (direct-gate-sample u.written)
13298− ?~ written-sample ~
13299− ?. ?=(%cell -.u.written-sample) ~
13300− ?. ?=([* * * * ~] items.u.written-sample) ~
13301− =/ checked=(map term def)
13302− (~(put by (direct-checked-gates ds env)) update.parts update-def)
13304− (turn molds.u.prelude.initial |=(x=[name=term template=ischeme] [name.x template.x]))
13305− =/ scanned=(unit dgscan)
13306− (dg-all-env-ids (weld env (weld values.u.prelude.initial templates)) 32.768 ~)
13308− =. next.initial (dg-next-id ids.u.scanned 0)
13309− =/ update-state=istate (reserve-def-caps val.update-def initial)
13310− =/ sam=isample-result (infer-sample u.written-update env update-state)
13312− =/ actual-sample=itype (itype-normalize typ.p.sam sub.state.p.sam)
13313− ?. ?=(%cell -.actual-sample) ~
13314− =/ message=(unit itype)
13315− (direct-slot-body hed.actual-sample (direct-sample-name i.items.u.written-update))
13316− =/ model=(unit itype)
13317− (direct-slot-body tal.actual-sample (direct-sample-name i.t.items.u.written-update))
13320− =/ cmd=(unit itype) (template-apply u.command ~[u.message])
13322− =/ command-result=(unit itype) (template-apply u.list-template ~[u.cmd])
13323− ?~ command-result ~
13324− =/ product=itype [%cell u.model u.command-result]
13325− =/ instance=[typ=itype state=istate] (instantiate-scheme u.program state.p.sam)
13326− ?. ?=(%fn -.typ.instance) ~
13327− ?. ?=(%cell -.sample.typ.instance) ~
13328− ?. ?=(%cell -.tal.sample.typ.instance) ~
13329− =/ expected-update=(unit itype)
13330− (direct-slot-body hed.tal.sample.typ.instance (direct-sample-name i.t.items.u.written-sample))
13331− ?~ expected-update ~
13332− ?. ?=(%fn -.u.expected-update) ~
13333− :: Sample binders are not value faces. Strip only those two slot faces
13334− :: for the invariant canonical-gate proof; the source-faced gate is still
13335− :: used by the complete positional call and final ordinary result cast.
13336− =/ canonical-candidate=itype [%fn [%cell u.message u.model] product]
13338− (direct-invariant canonical-candidate u.expected-update sub.state.instance next.state.instance)
13339− ?. ?=(%ok -.gate-fit) ~
13341− (itype-normalize [%fn typ.p.sam product] sub.gate-fit)
13342− ?. ?=(%fn -.closed) ~
13343− :: The closed product no longer needs the canonical slot substitutions.
13344− :: Start the body at its ordinary sample state so existing branch retries
13345− :: keep their substitution guards, but retain the shared fresh-ID high water.
13346− =/ st=istate state.p.sam(next next.gate-fit, gate-defs checked, head-evidence heads)
13348− ?- -.val.update-def
13349− %gate body.val.update-def
13350− %gate-wide body.val.update-def
13353− =/ inferred=iresult
13354− (infer-call-context-arg body product.closed env.p.sam st (span-of body))
13355− ?: ?=(%| -.inferred) ~
13356− =/ product-fit=ifit
13357− (itype-fit typ.p.inferred product.closed sub.state.p.inferred next.state.p.inferred)
13358− ?. ?=(%ok -.product-fit) ~
13359− =/ merged-product=itype
13360− (itype-merge-faces typ.p.inferred product.closed sub.product-fit)
13361− =/ actual-cast=itype [%fn typ.p.sam merged-product]
13363− (itype-fit actual-cast closed sub.product-fit next.product-fit)
13364− ?. ?=(%ok -.cast) ~
13365− =/ merged=itype (itype-merge-faces actual-cast closed sub.cast)
13366− =/ adjusted=iresult
13367− [%& merged state.p.inferred(sub sub.cast, next next.cast)]
13368− =/ added=(unit iadded-definition)
13369− (add-supported-result update-def adjusted update-state env checked artifacts.resolution)
13371− =/ recovered=(unit ischeme) (ienv-lookup update.parts env.u.added)
13373− ?. ?=(~ vars.u.recovered) ~
13374− ?. ?=(~ (itype-vars typ.u.recovered)) ~
13375− `[env.u.added grouped.resolution artifacts.u.added]
13377−++ program-inferred-slot
13378− |= [typ=itype name=(unit term)]
13381− ?: &(?=(%face -.typ) =(name.typ u.name)) body.typ
13384−++ program-inferred-sample
13385− |= [typ=itype sam=sample]
13387− (program-inferred-slot typ (direct-sample-name sam))
13389−++ program-two-slot-names
13391− ^- (unit [first=(unit term) second=(unit term)])
13394− ?. ?=([* * ~] items.sam) ~
13395− `[(direct-sample-name i.items.sam) (direct-sample-name i.t.items.sam)]
13397− ?. ?=(%cell -.shape.sam) ~
13398− ?. ?=([* * ~] fields.shape.sam) ~
13399− `[(direct-field-name i.fields.shape.sam) (direct-field-name i.t.fields.shape.sam)]
13403−:: Read message/model from the checked update and its written source layout.
13404−:: The source names strip only top-level sample binder faces; nested value
13405−:: faces remain part of the canonical message and model.
13406−++ program-update-relation
13407− |= [name=term ds=(list def) env=ienv]
13408− ^- (unit [message=itype model=itype])
13409− =/ update=(unit ischeme) (ienv-lookup name env)
13411− ?. ?=(~ vars.u.update) ~
13412− ?. ?=(~ (itype-vars typ.u.update)) ~
13413− ?. ?=(%fn -.typ.u.update) ~
13414− ?. ?=(%cell -.sample.typ.u.update) ~
13415− =/ defs=(list def)
13416− (skim ds |=(d=def &(?=(%value -.d) =(name name.d))))
13417− ?. ?=([* ~] defs) ~
13418− =/ written=(unit sample) (direct-gate-sample i.defs)
13420− ?. ?=(%cell -.u.written) ~
13421− ?. ?=([* * ~] items.u.written) ~
13422− =/ message=(unit itype)
13423− (direct-slot-body hed.sample.typ.u.update (direct-sample-name i.items.u.written))
13424− =/ model=(unit itype)
13425− (direct-slot-body tal.sample.typ.u.update (direct-sample-name i.t.items.u.written))
13428− `[u.message u.model]
13430−:: Recover an unannotated direct subscription component from the checked
13431−:: update relation and canonical fourth program slot. This establishes only
13432−:: the value type; the final program watch proof remains separate.
13433−++ program-subs-context
13434− |= [parts=[init=term update=term view=term subs=term] ds=(list def) resolution=iresolved initial=istate]
13435− ^- (unit iresolved)
13436− =/ env=ienv env.resolution
13437− ?^ (ienv-lookup %main env) ~
13438− ?^ (ienv-lookup subs.parts env) ~
13439− =/ relation=(unit [message=itype model=itype])
13440− (program-update-relation update.parts ds env)
13442− =/ subs=(list def)
13443− (skim ds |=(d=def &(?=(%value -.d) =(subs.parts name.d))))
13444− ?. ?=([* ~] subs) ~
13445− =/ subs-def=def i.subs
13446− ?> ?=(%value -.subs-def)
13447− =/ written-subs=(unit sample) (direct-gate-sample subs-def)
13449− ?~ prelude.initial ~
13450− =/ program=(unit ischeme) (ienv-lookup %program values.u.prelude.initial)
13451− =/ sub=(unit ischeme) (find-jibb-mold %sub u.prelude.initial)
13452− =/ list-template=(unit ischeme) (find-jibb-mold %list u.prelude.initial)
13455− ?~ list-template ~
13456− =/ heads=(unit igate-prelude-evidence) (direct-prelude-evidence ds prelude.initial)
13458− =/ written=(unit def) (~(get by gates.u.heads) %program)
13460− =/ written-sample=(unit sample) (direct-gate-sample u.written)
13461− ?~ written-sample ~
13462− ?. ?=(%cell -.u.written-sample) ~
13463− ?. ?=([* * * * ~] items.u.written-sample) ~
13464− =/ checked=(map term def) (direct-checked-gates ds env)
13466− (turn molds.u.prelude.initial |=(x=[name=term template=ischeme] [name.x template.x]))
13467− =/ scanned=(unit dgscan)
13468− (dg-all-env-ids (weld env (weld values.u.prelude.initial templates)) 32.768 ~)
13470− =. next.initial (dg-next-id ids.u.scanned 0)
13471− =/ subs-state=istate (reserve-def-caps val.subs-def initial)
13472− =/ sam=isample-result (infer-sample u.written-subs env subs-state)
13474− =/ actual-model=itype (program-inferred-sample typ.p.sam u.written-subs)
13475− ?. ?=(~ (itype-vars actual-model)) ~
13476− ?: (itype-has-tag actual-model) ~
13478− (direct-invariant actual-model model.u.relation sub.state.p.sam next.state.p.sam)
13479− ?. ?=(%ok -.model-fit) ~
13480− =/ message-sub=(unit itype) (template-apply u.sub ~[message.u.relation])
13482− =/ product=(unit itype) (template-apply u.list-template ~[u.message-sub])
13484− =/ instance=[typ=itype state=istate]
13485− (instantiate-scheme u.program state.p.sam(sub sub.model-fit, next next.model-fit))
13486− ?. ?=(%fn -.typ.instance) ~
13487− ?. ?=(%cell -.sample.typ.instance) ~
13488− ?. ?=(%cell -.tal.sample.typ.instance) ~
13489− ?. ?=(%cell -.tal.tal.sample.typ.instance) ~
13490− =/ expected-subs=(unit itype)
13491− (direct-slot-body tal.tal.tal.sample.typ.instance (direct-sample-name i.t.t.t.items.u.written-sample))
13492− ?~ expected-subs ~
13493− ?. ?=(%fn -.u.expected-subs) ~
13494− =/ canonical=itype [%fn model.u.relation u.product]
13496− (direct-invariant canonical u.expected-subs sub.state.instance next.state.instance)
13497− ?. ?=(%ok -.gate-fit) ~
13499− (itype-normalize [%fn typ.p.sam u.product] sub.gate-fit)
13500− ?. ?=(%fn -.closed) ~
13503− %gate body.val.subs-def
13504− %gate-wide body.val.subs-def
13508− state.p.sam(next next.gate-fit, gate-defs checked, head-evidence heads)
13509− =/ inferred=iresult
13510− (infer-call-context-arg body product.closed env.p.sam st (span-of body))
13511− ?: ?=(%| -.inferred) ~
13512− =/ product-fit=ifit
13513− (itype-fit typ.p.inferred product.closed sub.state.p.inferred next.state.p.inferred)
13514− ?. ?=(%ok -.product-fit) ~
13515− =/ merged-product=itype
13516− (itype-merge-faces typ.p.inferred product.closed sub.product-fit)
13517− =/ actual-cast=itype [%fn typ.p.sam merged-product]
13519− (itype-fit actual-cast closed sub.product-fit next.product-fit)
13520− ?. ?=(%ok -.cast) ~
13521− =/ merged=itype (itype-merge-faces actual-cast closed sub.cast)
13522− =/ adjusted=iresult
13523− [%& merged state.p.inferred(sub sub.cast, next next.cast)]
13524− =/ added=(unit iadded-definition)
13525− (add-supported-result subs-def adjusted subs-state env checked artifacts.resolution)
13527− =/ recovered=(unit ischeme) (ienv-lookup subs.parts env.u.added)
13529− ?. ?=(~ vars.u.recovered) ~
13530− ?. ?=(~ (itype-vars typ.u.recovered)) ~
13531− `[env.u.added grouped.resolution artifacts.u.added]
13533−+$ iview-site [xs=expr mapper=term]
13534−++ program-view-site
13536− ^- (unit iview-site)
13537− =. e (program-transparent e)
13538− ?. ?=(%call -.e) ~
13539− ?. ?=([* ~] args.e) ~
13540− =/ each=expr (program-transparent head.e)
13541− ?. ?=(%wing -.each) ~
13542− ?. ?=([%each ~] names.each) ~
13543− =/ turned=expr (program-transparent i.args.e)
13544− ?. ?=(%call -.turned) ~
13545− ?. ?=([* * ~] args.turned) ~
13546− =/ turn=expr (program-transparent head.turned)
13547− ?. ?=(%wing -.turn) ~
13548− ?. ?=([%turn ~] names.turn) ~
13549− =/ xs=expr (program-transparent i.args.turned)
13550− ?. ?=(%wing -.xs) ~
13552− =/ mapper=(unit term) (program-main-wing i.t.args.turned)
13556−++ program-sample-binders
13563− %cell (zing (turn items.sam |=(s=sample (program-sample-binders s))))
13567−++ program-pattern-binders
13572− %cell (zing (turn items.pat |=(p=pattern (program-pattern-binders p))))
13576−++ program-view-sites-merge
13577− |= [a=(unit (list iview-site)) b=(unit (list iview-site))]
13578− ^- (unit (list iview-site))
13583−++ program-view-sites-exprs
13584− |= [xs=(list expr) locals=(list term)]
13585− ^- (unit (list iview-site))
13587− (program-view-sites-merge (program-view-sites i.xs locals) $(xs t.xs))
13589−++ program-view-sites-items
13590− |= [xs=(list item) locals=(list term)]
13591− ^- (unit (list iview-site))
13593− (program-view-sites-merge (program-view-sites val.i.xs locals) $(xs t.xs))
13595−++ program-view-sites-pieces
13596− |= [xs=(list piece) locals=(list term)]
13597− ^- (unit (list iview-site))
13599− =/ here=(unit (list iview-site))
13601− %expr (program-view-sites p.i.xs locals)
13604− (program-view-sites-merge here $(xs t.xs))
13606−++ program-view-sites-qsegs
13607− |= [xs=(list qseg) locals=(list term)]
13608− ^- (unit (list iview-site))
13610− =/ here=(unit (list iview-site))
13612− %expr (program-view-sites p.i.xs locals)
13615− (program-view-sites-merge here $(xs t.xs))
13617−++ program-view-sites-edits
13618− |= [xs=(list edit) locals=(list term)]
13619− ^- (unit (list iview-site))
13621− (program-view-sites-merge (program-view-sites val.i.xs locals) $(xs t.xs))
13623−++ program-view-sites-defs
13624− |= [xs=(list def) locals=(list term)]
13625− ^- (unit (list iview-site))
13627− =/ here=(unit (list iview-site))
13628− ?: ?=(%mold -.i.xs) `~
13629− (program-view-sites val.i.xs locals)
13630− (program-view-sites-merge here $(xs t.xs))
13632−++ program-view-sites-arms
13633− |= [xs=(list arm) locals=(list term)]
13634− ^- (unit (list iview-site))
13636− =/ nested=(list term) (weld (program-pattern-binders pat.i.xs) locals)
13637− (program-view-sites-merge (program-view-sites val.i.xs nested) $(xs t.xs))
13639−++ program-view-sites
13640− |= [e=expr locals=(list term)]
13641− ^- (unit (list iview-site))
13642− =/ site=(unit iview-site) (program-view-site e)
13644− =/ names=(list term) ~[%each %turn mapper.u.site]
13645− ?> ?=(%wing -.xs.u.site)
13646− =/ root=term (rear names.xs.u.site)
13647− ?: |((lien names |=(n=term (lien locals |=(x=term =(n x))))) (lien locals |=(x=term =(root x))))
13651− %str (program-view-sites-pieces pieces.e locals)
13652− %qath (program-view-sites-qsegs segs.e locals)
13653− %change (program-view-sites-edits edits.e locals)
13654− %pair (program-view-sites val.e locals)
13655− %unit (program-view-sites val.e locals)
13656− %group (program-view-sites inner.e locals)
13657− %list (program-view-sites-exprs items.e locals)
13658− %tuple (program-view-sites-items items.e locals)
13660− (program-view-sites body.e (weld (program-sample-binders sample.e) locals))
13662− (program-view-sites body.e (weld (program-sample-binders sample.e) locals))
13664− (program-view-sites-merge (program-view-sites head.e locals) (program-view-sites-exprs args.e locals))
13665− %cast (program-view-sites val.e locals)
13667− (program-view-sites-merge (program-view-sites val.e locals) (program-view-sites then.e locals))
13669− (program-view-sites-merge (program-view-sites subject.e locals) (program-view-sites-arms arms.e locals))
13671− =/ nested=(list term) (weld (global-value-names defs.e) locals)
13672− (program-view-sites-merge (program-view-sites-defs defs.e nested) (program-view-sites final.e nested))
13676−++ program-union-tag-case
13677− |= [expected=itype tag=@]
13679− ?. ?=(%union -.expected) ~
13680− =/ remaining=(list itype) cases.expected
13681− =/ found=(unit itype) ~
13682− =/ seen=(set @) *(set @)
13684− ?~ remaining found
13685− =/ case=itype i.remaining
13687− ?: ?=(%const -.case) `val.literal.case
13688− ?. ?=(%cell -.case) ~
13689− ?. ?=(%const -.hed.case) ~
13690− `val.literal.hed.case
13692− ?: (~(has in:..zuse seen) u.head) ~
13693− =. seen (~(put in:..zuse seen) u.head)
13694− =? found =(tag u.head)
13696− $(remaining t.remaining)
13698−++ program-single-case-fit
13699− |= [actual=itype expected=itype sub=isub next=@ud]
13701− =. actual (itype-normalize actual sub)
13702− =. expected (itype-normalize expected sub)
13703− ?. ?=(%union -.expected) [%unknown ~]
13704− =/ found=(unit itype)
13705− ?: ?=(%const -.actual) `actual
13706− ?: ?=(%tag -.actual) `actual
13707− ?: ?=(%cell -.actual) `actual
13708− ?. ?=(%union -.actual) ~
13709− ?. ?=([* ~] cases.actual) ~
13711− ?~ found [%unknown ~]
13712− =/ case=itype u.found
13714− ?: ?=(%const -.case) `literal.case
13715− ?: ?=(%tag -.case) `literal.case
13716− ?. ?=(%cell -.case) ~
13717− =/ head=itype (projection-field-target hed.case)
13718− ?: ?=(%const -.head) `literal.head
13719− ?: ?=(%tag -.head) `literal.head
13721− ?~ tag [%unknown ~]
13722− =/ chosen=(unit itype) (program-union-tag-case expected val.u.tag)
13723− ?~ chosen [%unknown ~]
13724− ?: |(?=(%const -.case) ?=(%tag -.case))
13725− ?. ?=(%const -.u.chosen) [%unknown ~]
13726− (itype-fit case u.chosen sub next)
13727− ?. ?=(%cell -.case) [%unknown ~]
13728− ?. ?=(%cell -.u.chosen) [%unknown ~]
13729− =/ head-fit=ifit (itype-fit hed.case hed.u.chosen sub next)
13730− ?. ?=(%ok -.head-fit) head-fit
13731− (itype-fit tal.case tal.u.chosen sub.head-fit next.head-fit)
13733−++ program-single-generic-fit
13734− |= [actual=itype expected=itype sub=isub next=@ud]
13736− =. actual (itype-normalize actual sub)
13737− =. expected (itype-normalize expected sub)
13738− ?. &(?=(%union -.actual) ?=(%union -.expected)) [%unknown ~]
13739− ?~ origin.actual [%unknown ~]
13740− ?. =(origin.actual origin.expected) [%unknown ~]
13741− ?. ?=([* ~] args.actual) [%unknown ~]
13742− ?. ?=([* ~] args.expected) [%unknown ~]
13743− =/ argument-fit=ifit (direct-invariant i.args.actual i.args.expected sub next)
13744− ?: ?=(%ok -.argument-fit) argument-fit
13745− (program-single-case-fit i.args.actual i.args.expected sub next)
13747−++ program-keyed-product-fit
13748− |= [actual=itype expected=itype element=ischeme sub=isub next=@ud]
13750− =. actual (itype-normalize actual sub)
13751− =. expected (itype-normalize expected sub)
13752− ?. &(?=(%cell -.actual) ?=(%cell -.expected)) [%unknown ~]
13754− (itype-fit (projection-field-target hed.actual) (projection-field-target hed.expected) sub next)
13755− ?. ?=(%ok -.key-fit) key-fit
13756− =/ actual-el=itype
13757− (itype-normalize (projection-field-target tal.actual) sub.key-fit)
13758− =/ expected-el=itype
13759− (itype-normalize (projection-field-target tal.expected) sub.key-fit)
13760− ?. &(?=(%union -.actual-el) ?=(%union -.expected-el)) [%unknown ~]
13761− ?. =(origin.actual-el origin.expected-el) [%unknown ~]
13762− ?. ?=([* ~] args.actual-el) [%unknown ~]
13763− ?. ?=([* ~] args.expected-el) [%unknown ~]
13764− =/ canonical-actual=(unit itype)
13765− (template-apply element ~[i.args.actual-el])
13766− =/ canonical-expected=(unit itype)
13767− (template-apply element ~[i.args.expected-el])
13768− ?~ canonical-actual [%unknown ~]
13769− ?~ canonical-expected [%unknown ~]
13770− =/ actual-check=ifit
13771− (direct-invariant actual-el u.canonical-actual sub.key-fit next.key-fit)
13772− ?. ?=(%ok -.actual-check) actual-check
13773− =/ expected-check=ifit
13774− (direct-invariant expected-el u.canonical-expected sub.actual-check next.actual-check)
13775− ?. ?=(%ok -.expected-check) expected-check
13777− (program-single-case-fit i.args.actual-el i.args.expected-el sub.expected-check next.expected-check)
13780−:: A direct view without a keyed each/turn site still needs the message type
13781−:: from the checked update. Recover only that closed component; final main
13782−:: checking remains the canonical program-kind boundary.
13783−++ program-plain-view-context
13784− |= [parts=[init=term update=term view=term subs=term] ds=(list def) resolution=iresolved initial=istate]
13785− ^- (unit iresolved)
13786− =/ env=ienv env.resolution
13787− ?^ (ienv-lookup %main env) ~
13788− ?^ (ienv-lookup view.parts env) ~
13789− =/ relation=(unit [message=itype model=itype])
13790− (program-update-relation update.parts ds env)
13792− =/ views=(list def)
13793− (skim ds |=(d=def &(?=(%value -.d) =(view.parts name.d))))
13794− ?. ?=([* ~] views) ~
13795− =/ view-def=def i.views
13796− ?> ?=(%value -.view-def)
13797− =/ written-view=(unit sample) (direct-gate-sample view-def)
13801− %gate body.val.view-def
13802− %gate-wide body.val.view-def
13805− =/ sites=(unit (list iview-site)) (program-view-sites body ~)
13808− ?~ prelude.initial ~
13809− ?~ (ienv-lookup %program values.u.prelude.initial) ~
13810− =/ element=(unit ischeme) (find-jibb-mold %element u.prelude.initial)
13812− =/ heads=(unit igate-prelude-evidence) (direct-prelude-evidence ds prelude.initial)
13814− ?~ (~(get by gates.u.heads) %program) ~
13815− =/ checked=(map term def) (direct-checked-gates ds env)
13817− (turn molds.u.prelude.initial |=(x=[name=term template=ischeme] [name.x template.x]))
13818− =/ scanned=(unit dgscan)
13819− (dg-all-env-ids (weld env (weld values.u.prelude.initial templates)) 32.768 ~)
13821− =. next.initial (dg-next-id ids.u.scanned 0)
13822− =/ view-state=istate (reserve-def-caps val.view-def initial)
13823− =/ sam=isample-result (infer-sample u.written-view env view-state)
13825− =/ actual-model=itype (program-inferred-sample typ.p.sam u.written-view)
13826− ?. ?=(~ (itype-vars actual-model)) ~
13827− ?: (itype-has-tag actual-model) ~
13829− (direct-invariant actual-model model.u.relation sub.state.p.sam next.state.p.sam)
13830− ?. ?=(%ok -.model-fit) ~
13831− =/ product=(unit itype) (template-apply u.element ~[message.u.relation])
13834− state.p.sam(sub sub.model-fit, next next.model-fit, gate-defs checked, head-evidence heads)
13835− =/ inferred=iresult
13836− (infer-call-context-arg body u.product env.p.sam st (span-of body))
13837− ?: ?=(%| -.inferred) ~
13838− =/ product-fit=ifit
13839− (itype-fit typ.p.inferred u.product sub.state.p.inferred next.state.p.inferred)
13840− ?. ?=(%ok -.product-fit) ~
13841− =/ merged-product=itype
13842− (itype-merge-faces typ.p.inferred u.product sub.product-fit)
13843− =/ actual-cast=itype [%fn typ.p.sam merged-product]
13844− =/ closed=itype [%fn typ.p.sam u.product]
13846− (itype-fit actual-cast closed sub.product-fit next.product-fit)
13847− ?. ?=(%ok -.cast) ~
13848− =/ merged=itype (itype-merge-faces actual-cast closed sub.cast)
13849− =/ adjusted=iresult
13850− [%& merged state.p.inferred(sub sub.cast, next next.cast)]
13851− =/ added=(unit iadded-definition)
13852− (add-supported-result view-def adjusted view-state env checked artifacts.resolution)
13854− =/ recovered=(unit ischeme) (ienv-lookup view.parts env.u.added)
13856− ?. ?=(~ vars.u.recovered) ~
13857− ?. ?=(~ (itype-vars typ.u.recovered)) ~
13858− `[env.u.added grouped.resolution artifacts.u.added]
13860−:: Recover exactly one direct keyed each/turn row mapper, then its view.
13861−:: The prelude's own each and turn schemes determine the mapper gate: the
13862−:: key is inferred from the mapper body, never selected by this recovery.
13863−++ program-view-context
13864− |= [parts=[init=term update=term view=term subs=term] ds=(list def) resolution=iresolved initial=istate]
13865− ^- (unit iresolved)
13866− =/ env=ienv env.resolution
13867− ?^ (ienv-lookup %main env) ~
13868− ?^ (ienv-lookup view.parts env) ~
13869− =/ relation=(unit [message=itype model=itype])
13870− (program-update-relation update.parts ds env)
13872− =/ views=(list def)
13873− (skim ds |=(d=def &(?=(%value -.d) =(view.parts name.d))))
13874− ?. ?=([* ~] views) ~
13875− =/ view-def=def i.views
13876− ?> ?=(%value -.view-def)
13877− =/ written-view=(unit sample) (direct-gate-sample view-def)
13881− %gate body.val.view-def
13882− %gate-wide body.val.view-def
13885− =/ sites=(unit (list iview-site)) (program-view-sites view-body ~)
13887− ?. ?=([* ~] u.sites) ~
13888− =/ site=iview-site i.u.sites
13889− =/ component-names=(list term) ~[init.parts update.parts view.parts subs.parts]
13890− ?: (lien component-names |=(n=term =(n mapper.site))) ~
13891− ?^ (ienv-lookup mapper.site env) ~
13892− =/ mappers=(list def)
13893− (skim ds |=(d=def &(?=(%value -.d) =(mapper.site name.d))))
13894− ?. ?=([* ~] mappers) ~
13895− =/ mapper-def=def i.mappers
13896− ?> ?=(%value -.mapper-def)
13897− =/ written-mapper=(unit sample) (direct-gate-sample mapper-def)
13898− ?~ written-mapper ~
13899− ?~ prelude.initial ~
13900− =/ program=(unit ischeme) (ienv-lookup %program values.u.prelude.initial)
13901− =/ each-scheme=(unit ischeme) (ienv-lookup %each values.u.prelude.initial)
13902− =/ turn-scheme=(unit ischeme) (ienv-lookup %turn values.u.prelude.initial)
13903− =/ element=(unit ischeme) (find-jibb-mold %element u.prelude.initial)
13904− =/ list-template=(unit ischeme) (find-jibb-mold %list u.prelude.initial)
13909− ?~ list-template ~
13910− =/ heads=(unit igate-prelude-evidence) (direct-prelude-evidence ds prelude.initial)
13912− =/ written-program=(unit def) (~(get by gates.u.heads) %program)
13913− =/ written-each=(unit def) (~(get by gates.u.heads) %each)
13914− =/ written-turn=(unit def) (~(get by gates.u.heads) %turn)
13915− ?~ written-program ~
13918− =/ program-sample=(unit sample) (direct-gate-sample u.written-program)
13919− =/ each-sample=(unit sample) (direct-gate-sample u.written-each)
13920− =/ turn-sample=(unit sample) (direct-gate-sample u.written-turn)
13921− ?~ program-sample ~
13924− ?. ?=(%cell -.u.program-sample) ~
13925− ?. ?=([* * * * ~] items.u.program-sample) ~
13926− =/ turn-names=(unit [first=(unit term) second=(unit term)])
13927− (program-two-slot-names u.turn-sample)
13929− =/ checked=(map term def) (direct-checked-gates ds env)
13931− (turn molds.u.prelude.initial |=(x=[name=term template=ischeme] [name.x template.x]))
13932− =/ scanned=(unit dgscan)
13933− (dg-all-env-ids (weld env (weld values.u.prelude.initial templates)) 32.768 ~)
13935− =. next.initial (dg-next-id ids.u.scanned 0)
13936− =/ view-state=istate (reserve-def-caps val.view-def initial)
13937− =/ sam=isample-result (infer-sample u.written-view env view-state)
13939− =/ actual-model=itype (program-inferred-sample typ.p.sam u.written-view)
13941− (direct-invariant actual-model model.u.relation sub.state.p.sam next.state.p.sam)
13942− ?. ?=(%ok -.model-fit) ~
13943− =/ xs-result=iresult
13944− (infer-fragment xs.site env.p.sam state.p.sam(sub sub.model-fit, next next.model-fit))
13945− ?: ?=(%| -.xs-result) ~
13946− =/ element-var=itype [%var next.state.p.xs-result]
13947− =/ list-a=(unit itype) (template-apply u.list-template ~[element-var])
13950− (itype-fit typ.p.xs-result u.list-a sub.state.p.xs-result +(next.state.p.xs-result))
13951− ?. ?=(%ok -.xs-fit) ~
13952− =/ closed-xs=itype (itype-normalize u.list-a sub.xs-fit)
13953− ?^ (itype-vars closed-xs) ~
13954− ?: (itype-has-tag closed-xs) ~
13955− =/ each-instance=[typ=itype state=istate]
13956− (instantiate-scheme u.each-scheme state.p.xs-result(sub sub.xs-fit, next next.xs-fit))
13957− ?. ?=(%fn -.typ.each-instance) ~
13958− =/ turn-instance=[typ=itype state=istate]
13959− (instantiate-scheme u.turn-scheme state.each-instance)
13960− ?. ?=(%fn -.typ.turn-instance) ~
13961− ?. ?=(%cell -.sample.typ.turn-instance) ~
13962− =/ element-message=(unit itype)
13963− (template-apply u.element ~[message.u.relation])
13964− ?~ element-message ~
13966− (itype-fit product.typ.each-instance u.element-message sub.state.turn-instance next.state.turn-instance)
13967− ?. ?=(%ok -.each-fit) ~
13968− =/ each-input=itype
13969− (program-inferred-sample sample.typ.each-instance u.each-sample)
13971− (itype-fit product.typ.turn-instance each-input sub.each-fit next.each-fit)
13972− ?. ?=(%ok -.turn-fit) ~
13973− =/ turn-list=itype
13974− (program-inferred-slot hed.sample.typ.turn-instance first.u.turn-names)
13976− (itype-fit closed-xs turn-list sub.turn-fit next.turn-fit)
13977− ?. ?=(%ok -.list-fit) ~
13978− =/ mapper-type=itype
13979− (program-inferred-slot tal.sample.typ.turn-instance second.u.turn-names)
13980− =/ expected-mapper=itype (itype-normalize mapper-type sub.list-fit)
13981− ?. ?=(%fn -.expected-mapper) ~
13982− ?^ (itype-vars sample.expected-mapper) ~
13983− ?: (itype-has-tag sample.expected-mapper) ~
13984− :: These faces come from the source-backed each sample. Keeping them in
13985− :: the expected mapper product lets ordinary tuple inference supply key/el.
13986− ?. ?=(%cell -.product.expected-mapper) ~
13987− ?. ?=(%face -.hed.product.expected-mapper) ~
13988− ?. =(%key name.hed.product.expected-mapper) ~
13989− ?. ?=(%face -.tal.product.expected-mapper) ~
13990− ?. =(%el name.tal.product.expected-mapper) ~
13991− =/ mapper-state=istate
13992− (reserve-def-caps val.mapper-def initial(next next.list-fit))
13993− =/ mapper-sam=isample-result (infer-sample u.written-mapper env mapper-state)
13994− ?: ?=(%| -.mapper-sam) ~
13995− =/ mapper-input=itype (program-inferred-sample typ.p.mapper-sam u.written-mapper)
13996− =/ mapper-sample-fit=ifit
13997− (direct-invariant mapper-input sample.expected-mapper sub.state.p.mapper-sam next.state.p.mapper-sam)
13998− ?. ?=(%ok -.mapper-sample-fit) ~
13999− =/ mapper-product=itype
14000− (itype-normalize product.expected-mapper sub.mapper-sample-fit)
14001− =/ mapper-body=expr
14002− ?- -.val.mapper-def
14003− %gate body.val.mapper-def
14004− %gate-wide body.val.mapper-def
14007− =/ mapper-inferred=iresult
14008− (infer-call-context-arg mapper-body mapper-product env.p.mapper-sam state.p.mapper-sam(sub sub.mapper-sample-fit, next next.mapper-sample-fit) (span-of mapper-body))
14009− ?: ?=(%| -.mapper-inferred) ~
14010− =/ ordinary-product-fit=ifit
14011− (itype-fit typ.p.mapper-inferred mapper-product sub.state.p.mapper-inferred next.state.p.mapper-inferred)
14012− =/ mapper-product-fit=ifit
14013− ?: ?=(%ok -.ordinary-product-fit) ordinary-product-fit
14014− (program-keyed-product-fit typ.p.mapper-inferred mapper-product u.element sub.state.p.mapper-inferred next.state.p.mapper-inferred)
14015− ?. ?=(%ok -.mapper-product-fit) ~
14016− =/ closed-mapper-product=itype
14017− (itype-normalize mapper-product sub.mapper-product-fit)
14018− ?^ (itype-vars closed-mapper-product) ~
14019− ?: (itype-has-tag closed-mapper-product) ~
14020− =/ merged-mapper-product=itype
14021− (itype-merge-faces typ.p.mapper-inferred closed-mapper-product sub.mapper-product-fit)
14022− =/ mapper-cast=itype [%fn typ.p.mapper-sam merged-mapper-product]
14023− =/ closed-mapper=itype [%fn typ.p.mapper-sam closed-mapper-product]
14024− =/ mapper-cast-fit=ifit
14025− (itype-fit mapper-cast closed-mapper sub.mapper-product-fit next.mapper-product-fit)
14026− ?. ?=(%ok -.mapper-cast-fit) ~
14027− =/ merged-mapper=itype
14028− (itype-merge-faces mapper-cast closed-mapper sub.mapper-cast-fit)
14029− =/ mapper-adjusted=iresult
14030− [%& merged-mapper state.p.mapper-inferred(sub sub.mapper-cast-fit, next next.mapper-cast-fit)]
14031− =/ mapper-added=(unit iadded-definition)
14032− (add-supported-result mapper-def mapper-adjusted mapper-state env checked artifacts.resolution)
14034− =/ mapper-scheme=(unit ischeme) (ienv-lookup mapper.site env.u.mapper-added)
14035− ?~ mapper-scheme ~
14036− ?. ?=(~ vars.u.mapper-scheme) ~
14037− ?. ?=(~ (itype-vars typ.u.mapper-scheme)) ~
14038− =/ program-instance=[typ=itype state=istate]
14039− (instantiate-scheme u.program state.p.sam(next next.mapper-cast-fit))
14040− ?. ?=(%fn -.typ.program-instance) ~
14041− ?. ?=(%cell -.sample.typ.program-instance) ~
14042− ?. ?=(%cell -.tal.sample.typ.program-instance) ~
14043− ?. ?=(%cell -.tal.tal.sample.typ.program-instance) ~
14044− =/ expected-view=(unit itype)
14045− (direct-slot-body hed.tal.tal.sample.typ.program-instance (direct-sample-name i.t.t.items.u.program-sample))
14046− ?~ expected-view ~
14047− ?. ?=(%fn -.u.expected-view) ~
14048− =/ canonical-view=itype [%fn model.u.relation u.element-message]
14050− (direct-invariant canonical-view u.expected-view sub.state.program-instance next.state.program-instance)
14051− ?. ?=(%ok -.view-fit) ~
14052− =/ closed-view=itype
14053− (itype-normalize [%fn typ.p.sam u.element-message] sub.view-fit)
14054− ?. ?=(%fn -.closed-view) ~
14055− =/ view-env=ienv [[mapper.site u.mapper-scheme] env.p.sam]
14056− =/ final-view-state=istate
14057− (reserve-def-caps val.view-def state.p.sam(next next.view-fit, gate-defs checked.u.mapper-added, head-evidence heads))
14058− =/ inferred=iresult
14059− (infer-call-context-arg view-body product.closed-view view-env final-view-state (span-of view-body))
14060− ?: ?=(%| -.inferred) ~
14061− =/ product-fit=ifit
14062− (itype-fit typ.p.inferred product.closed-view sub.state.p.inferred next.state.p.inferred)
14063− ?. ?=(%ok -.product-fit) ~
14064− =/ merged-product=itype
14065− (itype-merge-faces typ.p.inferred product.closed-view sub.product-fit)
14066− =/ actual-cast=itype [%fn typ.p.sam merged-product]
14068− (itype-fit actual-cast closed-view sub.product-fit next.product-fit)
14069− ?. ?=(%ok -.cast) ~
14070− =/ merged=itype (itype-merge-faces actual-cast closed-view sub.cast)
14071− =/ adjusted=iresult
14072− [%& merged state.p.inferred(sub sub.cast, next next.cast)]
14073− =/ added=(unit iadded-definition)
14074− (add-supported-result view-def adjusted final-view-state env.u.mapper-added checked.u.mapper-added artifacts.u.mapper-added)
14076− =/ recovered=(unit ischeme) (ienv-lookup view.parts env.u.added)
14078− ?. ?=(~ vars.u.recovered) ~
14079− ?. ?=(~ (itype-vars typ.u.recovered)) ~
14080− `[env.u.added grouped.resolution artifacts.u.added]
14082−++ program-init-null-sample
14085− =/ written=(unit sample) (direct-gate-sample d)
14087− ?. ?=(%bare -.u.written) |
14088− =/ sh=shape shape.u.written
14089− ?. ?=(%const -.sh) |
14090− =(%null form.lit.sh)
14092−:: The tuple-ending-null initializer retry above intentionally keeps its own
14093−:: boundary. A direct null-sample initializer can instead receive the closed
14094−:: model already established by update, view and subscriptions.
14095−++ program-plain-init-context
14096− |= [parts=[init=term update=term view=term subs=term] ds=(list def) resolution=iresolved initial=istate]
14097− ^- (unit iresolved)
14098− =/ env=ienv env.resolution
14099− ?^ (ienv-lookup %main env) ~
14100− ?^ (ienv-lookup init.parts env) ~
14101− ?~ (ienv-lookup update.parts env) ~
14102− ?~ (ienv-lookup view.parts env) ~
14103− ?~ (ienv-lookup subs.parts env) ~
14104− =/ relation=(unit [message=itype model=itype])
14105− (program-update-relation update.parts ds env)
14107− =/ inits=(list def)
14108− (skim ds |=(d=def &(?=(%value -.d) =(init.parts name.d))))
14109− ?. ?=([* ~] inits) ~
14110− =/ init-def=def i.inits
14111− ?> ?=(%value -.init-def)
14112− ?. (program-init-null-sample init-def) ~
14113− =/ written=(unit sample) (direct-gate-sample init-def)
14117− %gate body.val.init-def
14118− %gate-wide body.val.init-def
14121− ?~ prelude.initial ~
14122− ?~ (ienv-lookup %program values.u.prelude.initial) ~
14123− =/ heads=(unit igate-prelude-evidence) (direct-prelude-evidence ds prelude.initial)
14125− ?~ (~(get by gates.u.heads) %program) ~
14126− =/ checked=(map term def) (direct-checked-gates ds env)
14128− (turn molds.u.prelude.initial |=(x=[name=term template=ischeme] [name.x template.x]))
14129− =/ scanned=(unit dgscan)
14130− (dg-all-env-ids (weld env (weld values.u.prelude.initial templates)) 32.768 ~)
14132− =. next.initial (dg-next-id ids.u.scanned 0)
14133− =/ init-state=istate (reserve-def-caps val.init-def initial)
14134− =/ sam=isample-result (infer-sample u.written env init-state)
14136− ?. ?=(~ (itype-vars typ.p.sam)) ~
14137− ?: (itype-has-tag typ.p.sam) ~
14138− =/ st=istate state.p.sam(gate-defs checked, head-evidence heads)
14139− =/ inferred=iresult
14140− (infer-call-context-arg body model.u.relation env.p.sam st (span-of body))
14141− ?: ?=(%| -.inferred) ~
14142− =/ product-fit=ifit
14143− (itype-fit typ.p.inferred model.u.relation sub.state.p.inferred next.state.p.inferred)
14144− ?. ?=(%ok -.product-fit) ~
14145− =/ merged-product=itype
14146− (itype-merge-faces typ.p.inferred model.u.relation sub.product-fit)
14147− =/ actual-cast=itype [%fn typ.p.sam merged-product]
14148− =/ closed=itype [%fn typ.p.sam model.u.relation]
14150− (itype-fit actual-cast closed sub.product-fit next.product-fit)
14151− ?. ?=(%ok -.cast) ~
14152− =/ merged=itype (itype-merge-faces actual-cast closed sub.cast)
14153− =/ adjusted=iresult
14154− [%& merged state.p.inferred(sub sub.cast, next next.cast)]
14155− =/ added=(unit iadded-definition)
14156− (add-supported-result init-def adjusted init-state env checked artifacts.resolution)
14158− =/ recovered=(unit ischeme) (ienv-lookup init.parts env.u.added)
14160− ?. ?=(~ vars.u.recovered) ~
14161− ?. ?=(~ (itype-vars typ.u.recovered)) ~
14162− `[env.u.added grouped.resolution artifacts.u.added]
14164−:: Recover only the initializer of an already recognized direct program main.
14165−:: The derived call is evidence for an ordinary init/main retry, never an
14166−:: interface to publish on its own. Any failure returns the original resolution.
14167−++ program-init-context
14168− |= [main=def parts=[init=term update=term view=term subs=term] ds=(list def) resolution=iresolved initial=istate]
14169− ^- (unit iresolved)
14170− =/ env=ienv env.resolution
14171− ?^ (ienv-lookup %main env) ~
14172− ?^ (ienv-lookup init.parts env) ~
14173− =/ update=(unit ischeme) (ienv-lookup update.parts env)
14174− =/ view=(unit ischeme) (ienv-lookup view.parts env)
14175− =/ subs=(unit ischeme) (ienv-lookup subs.parts env)
14179− =/ inits=(list def)
14180− (skim ds |=(d=def &(?=(%value -.d) =(init.parts name.d))))
14181− ?. ?=([* ~] inits) ~
14182− =/ init-def=def i.inits
14183− ?> ?=(%value -.init-def)
14184− ?. (program-init-tuple-null init-def) ~
14185− =/ args=(unit (list expr)) (program-main-args main)
14187− ?~ prelude.initial ~
14188− =/ program=(unit ischeme) (ienv-lookup %program values.u.prelude.initial)
14190− =/ heads=(unit igate-prelude-evidence) (direct-prelude-evidence ds prelude.initial)
14192− =/ written=(unit def) (~(get by gates.u.heads) %program)
14194− =/ written-sample=(unit sample) (direct-gate-sample u.written)
14195− ?~ written-sample ~
14196− ?. ?=(%cell -.u.written-sample) ~
14197− ?~ items.u.written-sample ~
14198− =/ checked=(map term def) (direct-checked-gates ds env)
14200− (turn molds.u.prelude.initial |=(x=[name=term template=ischeme] [name.x template.x]))
14201− =/ scanned=(unit dgscan)
14202− (dg-all-env-ids (weld env (weld values.u.prelude.initial templates)) 32.768 ~)
14204− =. next.initial (dg-next-id ids.u.scanned 0)
14205− =/ instance=[typ=itype state=istate] (instantiate-scheme u.program initial)
14206− ?. ?=(%fn -.typ.instance) ~
14207− ?. ?=(%cell -.sample.typ.instance) ~
14208− =/ expected-init=(unit itype)
14209− (direct-slot-body hed.sample.typ.instance (direct-sample-name i.items.u.written-sample))
14210− ?~ expected-init ~
14211− ?. ?=(%fn -.u.expected-init) ~
14212− ?. ?=(%var -.sample.u.expected-init) ~
14213− =/ data=@ud id.sample.u.expected-init
14214− =/ init-var=itype [%var next.state.instance]
14215− =/ st=istate state.instance(next +(next.state.instance))
14216− =/ up=[typ=itype state=istate] (instantiate-scheme u.update st)
14217− =/ vw=[typ=itype state=istate] (instantiate-scheme u.view state.up)
14218− =/ sb=[typ=itype state=istate] (instantiate-scheme u.subs state.vw)
14219− =. st state.sb(gate-defs checked, head-evidence heads)
14220− =/ actual=itype [%cell init-var [%cell typ.up [%cell typ.vw typ.sb]]]
14222− (direct-positional-fit u.args items.u.written-sample actual sample.typ.instance env st sub.st next.st)
14223− ?. ?=(%ok -.fit) ~
14224− =/ actual-final=itype (itype-normalize actual sub.fit)
14225− =/ expected-final=itype (itype-normalize sample.typ.instance sub.fit)
14226− =/ open=(list @ud)
14227− (unique-type-vars (weld (itype-vars actual-final) (itype-vars expected-final)))
14228− ?. (levy open |=(n=@ud =(data n))) ~
14229− ?: |((itype-has-tag actual-final) (itype-has-tag expected-final)) ~
14231− (direct-positional-fit u.args items.u.written-sample actual sample.typ.instance env st sub.fit next.fit)
14232− ?. ?=(%ok -.replay) ~
14233− ?. &(=(sub.fit sub.replay) =(next.fit next.replay)) ~
14234− =/ expected=itype (itype-normalize u.expected-init sub.fit)
14235− ?. ?=(%fn -.expected) ~
14236− =. st st(sub sub.fit, next next.fit)
14237− =/ init-state=istate (reserve-def-caps val.init-def st)
14238− =/ inferred=iresult (infer-fragment val.init-def env init-state)
14239− =? inferred ?=(%| -.inferred) (infer-recursive-gate init-def env init-state)
14240− ?: ?=(%| -.inferred) ~
14241− ?. ?=(%fn -.typ.p.inferred) ~
14242− ?^ (itype-vars sample.typ.p.inferred) ~
14244− (itype-fit sample.typ.p.inferred sample.expected sub.state.p.inferred next.state.p.inferred)
14245− ?. ?=(%ok -.data-fit) ~
14246− =/ closed=itype (itype-normalize expected sub.data-fit)
14247− ?. ?=(%fn -.closed) ~
14248− :: Resolve the ordinary tuple cast first, then check the complete gate.
14249− :: General function fit remains unchanged; only this recovered candidate
14250− :: receives the derived result context before its whole-type cast fit.
14251− =/ product-fit=ifit
14252− (itype-fit product.typ.p.inferred product.closed sub.data-fit next.data-fit)
14253− ?. ?=(%ok -.product-fit) ~
14255− (itype-merge-faces product.typ.p.inferred product.closed sub.product-fit)
14256− =/ actual-cast=itype [%fn sample.typ.p.inferred product]
14258− (itype-fit actual-cast closed sub.product-fit next.product-fit)
14259− ?. ?=(%ok -.cast) ~
14260− =/ merged=itype (itype-merge-faces actual-cast closed sub.cast)
14261− =/ adjusted=iresult
14262− [%& merged state.p.inferred(sub sub.cast, next next.cast)]
14263− =/ added=(unit iadded-definition)
14264− (add-supported-result init-def adjusted init-state env checked artifacts.resolution)
14266− =/ recovered=(unit ischeme) (ienv-lookup init.parts env.u.added)
14268− ?. ?=(~ vars.u.recovered) ~
14269− ?. ?=(~ (itype-vars typ.u.recovered)) ~
14270− `[env.u.added grouped.resolution artifacts.u.added]
14272−++ derived-poke-command-scheme
14273− |= [prelude=ifile action=itype]
14275− =/ prep=iprelude [prelude ~ ~]
14276− =/ raw=(unit ischeme) (compatible-raw-poke prep)
14278− =/ command=(unit ischeme) (find-jibb-mold %cmd prelude)
14279− =/ unit-template=(unit ischeme) (find-jibb-mold %unit prelude)
14281− ?~ unit-template ~
14282− ?. (standard-unit-template u.unit-template /lib/jibb/prelude/jibb) ~
14283− ?. ?=([@ ~] vars.u.command) ~
14284− ?. ?=(%union -.typ.u.command) ~
14285− ?. =(origin.typ.u.command `[/lib/jibb/prelude/jibb %cmd]) ~
14286− ?. (identity-union-parameters vars.u.command args.typ.u.command) ~
14287− =/ m=@ud i.vars.u.command
14288− ?: (itype-var-is-atom m typ.u.command) ~
14289− ?. (levy (itype-vars typ.u.command) |=(n=@ud =(n m))) ~
14290− ?: (itype-has-tag typ.u.command) ~
14291− =/ error=(unit itype) (template-apply u.unit-template ~[[%atom %t]])
14293− ?. ?=(%union -.typ.u.raw) ~
14294− =/ poke-case=itype
14295− [%cell [%const [%term %tas %poke '%poke']] [%cell [%face %p typ.u.raw(label `'raw-poke')] [%face %reply [%fn u.error [%var m]]]]]
14297− [%cell [%const [%term %tas %go '%go']] [%face %url [%atom %t]]]
14298− =/ wait-case=itype
14299− [%cell [%const [%term %tas %wait '%wait']] [%cell [%face %gap [%atom %dr]] [%face %msg [%var m]]]]
14301− [%cell [%const [%term %tas %now '%now']] [%face %reply [%fn [%atom %da] [%var m]]]]
14303− [%cell [%const [%term %tas %who '%who']] [%face %reply [%fn [%atom %p] [%var m]]]]
14304− ?. =(cases.typ.u.command ~[poke-case go-case wait-case now-case who-case]) ~
14305− =/ command-result=(unit itype) (template-apply u.command ~[[%var 0]])
14306− ?~ command-result ~
14307− `[[%fn [%cell action [%fn u.error [%var 0]]] u.command-result] ~[0]]
14309−++ store-derived-schemes
14310− |= [prelude=ifile values=(list term) molds=(list term) state=itype action=itype]
14311− ^- (unit [state=ischeme action=ischeme])
14312− =/ prep=iprelude [prelude values molds]
14313− =/ ask=(unit ischeme) (request-compatible-ask prep)
14315− ?^ (itype-vars state) ~
14316− ?^ (itype-vars action) ~
14317− ?: |((itype-has-tag state) (itype-has-tag action)) ~
14318− =/ result=(unit itype) (template-apply u.ask ~[[%var 0]])
14320− =/ request=ischeme [[%fn [%fn state [%var 0]] u.result] ~[0]]
14321− =/ constructor=(unit ischeme) (derived-poke-command-scheme prelude action)
14323− `[request u.constructor]
14325−++ program-subs-watch
14326− |= [d=def imports=ijimports graph=irequest-graph prelude=ifile]
14328− ?. ?=(%value -.d) |
14329− ?. |(?=(%gate -.val.d) ?=(%gate-wide -.val.d)) |
14333− %gate-wide body.val.d
14336− =. body (program-transparent body)
14337− ?. ?=(%list -.body) |
14338− ?. ?=([* ~] items.body) |
14339− =/ watch=expr (program-transparent i.items.body)
14340− ?. ?=(%tuple -.watch) |
14341− ?. ?=([* * ~] items.watch) |
14342− =/ tag=item i.items.watch
14343− =/ payload=item i.t.items.watch
14344− ?. &(?=(~ face.tag) ?=(~ face.payload)) |
14345− =/ tag-expr=expr (program-transparent val.tag)
14346− ?. ?=(%lit -.tag-expr) |
14347− ?. &(?=(%term form.lit.tag-expr) =(%watch val.lit.tag-expr)) |
14348− =/ request=expr (program-transparent val.payload)
14349− ?. ?=(%call -.request) |
14350− ?. ?=([* ~] args.request) |
14351− =/ head=expr (program-transparent head.request)
14352− ?. ?=(%wing -.head) |
14353− ?. ?=([@ @ ~] names.head) |
14354− =/ case=term i.names.head
14355− =/ face=term i.t.names.head
14356− =/ callback=expr (program-transparent i.args.request)
14357− ?. ?=(%ctor -.callback) |
14358− ?. ?=(%term form.tag.callback) |
14359− ?| ?=(^ (derived-request-member case face imports graph prelude))
14360− ?=(^ (derived-store-request-member case face imports graph prelude))
14363−:: Exact derived-member and request-evidence identity, shared by direct
14364−:: program watches and direct data-page loads. Only a plain request in the
14365−:: selected interface's own source-backed graph can establish this shape.
14366−++ derived-request-member
14367− |= [case=term face=term imports=ijimports graph=irequest-graph prelude=ifile]
14369− =/ selected=(list [face=term interface=ifile])
14370− (skim imports |=(j=[face=term interface=ifile] =(face face.j)))
14371− ?. ?=([* ~] selected) ~
14372− =/ iface=ifile interface.i.selected
14373− =/ member=(unit ischeme) (ienv-lookup case values.iface)
14376− =/ evidence=(list irequest-evidence)
14377− (skim requests.graph |=(r=irequest-evidence &(=(api-at.r at.iface) =(name.r case))))
14378− ?. ?=([* ~] evidence) ~
14379− =/ request-evidence=irequest-evidence i.evidence
14380− ?. =(u.source.iface api-source.request-evidence) ~
14381− ?. =(name.path.path.request-evidence case) ~
14383− ?. (lien requests.u.graph.iface |=(r=irequest-evidence =(r request-evidence))) ~
14384− ?. ?=(~ scry.path.path.request-evidence) ~
14385− ?. &(?=(~ diffs.path.request-evidence) ?=(~ diffs.path.path.request-evidence)) ~
14386− ?: (lien segments.path.path.request-evidence |=(p=pseg !?=(%knot -.p))) ~
14387− ?. ?=([@ ~] vars.u.member) ~
14388− =/ message=@ud i.vars.u.member
14389− ?. ?=(%fn -.typ.u.member) ~
14390− ?. ?=(%fn -.sample.typ.u.member) ~
14391− ?. =(sample.sample.typ.u.member full.path.request-evidence) ~
14392− ?. =(product.sample.typ.u.member [%var message]) ~
14393− =/ prep=iprelude [prelude prelude-values.graph prelude-molds.graph]
14394− =/ ask=(unit ischeme) (request-compatible-ask prep)
14396− =/ result=(unit itype) (template-apply u.ask ~[[%var message]])
14398− ?. =(product.typ.u.member u.result) ~
14401−:: Store state is watchable by definition, but only the actual derived member
14402−:: of the uniquely selected source-bound store interface proves that fact.
14403−++ derived-store-request-member
14404− |= [case=term face=term imports=ijimports graph=irequest-graph prelude=ifile]
14406− ?. =(%state case) ~
14407− =/ selected=(list [face=term interface=ifile])
14408− (skim imports |=(j=[face=term interface=ifile] =(face face.j)))
14409− ?. ?=([* ~] selected) ~
14410− =/ iface=ifile interface.i.selected
14411− =/ member=(unit ischeme) (ienv-lookup %state values.iface)
14414− =/ evidence=(list istore-request-evidence)
14415− (skim stores.graph |=(r=istore-request-evidence =(store-at.r at.iface)))
14416− ?. ?=([* ~] evidence) ~
14417− =/ request=istore-request-evidence i.evidence
14418− ?. =(u.source.iface source.request) ~
14420− ?. (lien stores.u.graph.iface |=(r=istore-request-evidence =(r request))) ~
14421− =/ derived=(unit [state=ischeme action=ischeme])
14422− (store-derived-schemes prelude prelude-values.graph prelude-molds.graph state.request action.request)
14424− ?. =(u.member state.u.derived) ~
14425− =/ constructor=(unit ischeme) (ienv-lookup action-name.request values.iface)
14427− ?. =(u.constructor action.u.derived) ~
14430−++ program-main-context
14431− |= [main=def ds=(list def) resolution=iresolved initial=istate]
14433− ?^ (ienv-lookup %main env.resolution) resolution
14434− =/ heads=(unit igate-prelude-evidence)
14435− (direct-prelude-evidence ds prelude.initial)
14436− ?~ heads resolution
14437− =/ checked=(map term def) (direct-checked-gates ds env.resolution)
14438− =/ completed=[env=ienv artifacts=(list iwidth-definition)]
14439− (add-supported-defs-core ~[main] checked heads env.resolution molds.initial globals.initial externals.initial surs.initial mark-externals.initial marks.initial jimports.initial reserved-molds.initial at.initial prelude.initial artifacts.resolution grec-index.initial)
14440− [env.completed grouped.resolution artifacts.completed]
14442−:: A static main may retain a generic element message in its ordinary
14443−:: scheme. Instantiate that scheme, specialize it to canonical element !!,
14444−:: and publish only the resulting closed scheme.
14445−++ static-main-specialized
14446− |= [env=ienv prelude=(unit ifile)]
14449− =/ element=(unit ischeme) (find-jibb-mold %element u.prelude)
14451− =/ main=(unit ischeme) (ienv-lookup %main env)
14453− =/ canonical=(unit itype) (template-apply u.element ~[[%empty ~]])
14455− =/ instance=[typ=itype state=istate] (instantiate-scheme u.main *istate)
14456− =/ fit=ifit (itype-fit typ.instance u.canonical ~ next.state.instance)
14457− ?. ?=(%ok -.fit) ~
14458− =/ closed=itype (itype-normalize typ.instance sub.fit)
14459− ?^ (itype-vars closed) ~
14460− ?: (itype-has-tag closed) ~
14461− ?. ?=(%union -.closed) ~
14462− ?. ?=(%union -.u.canonical) ~
14463− ?. &(=(origin.closed origin.u.canonical) =(args.closed args.u.canonical)) ~
14464− =/ exact=ifit (direct-invariant closed u.canonical ~ next.fit)
14465− ?. ?=(%ok -.exact) ~
14468−:: The load of a direct data page must itself be a direct gate whose
14469−:: transparent body is one plain derived request with a wing or ctor reply.
14470−++ page-load-derived
14471− |= [name=term ds=(list def) imports=ijimports graph=irequest-graph prelude=ifile]
14473− =/ loads=(list def)
14474− (skim ds |=(d=def &(?=(%value -.d) =(name name.d))))
14475− ?. ?=([* ~] loads) |
14476− =/ load=def i.loads
14477− ?> ?=(%value -.load)
14478− ?. |(?=(%gate -.val.load) ?=(%gate-wide -.val.load)) |
14481− %gate body.val.load
14482− %gate-wide body.val.load
14485− =. body (program-transparent body)
14486− ?. ?=(%call -.body) |
14487− ?. ?=([* ~] args.body) |
14488− =/ head=expr (program-transparent head.body)
14489− ?. ?=(%wing -.head) |
14490− ?. ?=([@ @ ~] names.head) |
14491− =/ reply=expr (program-transparent i.args.body)
14492− ?. ?| &(?=(%wing -.reply) ?=([@ ~] names.reply))
14493− &(?=(%ctor -.reply) ?=(%term form.tag.reply))
14496− ?=(^ (derived-request-member i.names.head i.t.names.head imports graph prelude))
14498−++ page-main-closed
14499− |= [parts=[load=term view=term] ds=(list def) env=ienv prelude=(unit ifile) imports=ijimports graph=irequest-graph]
14502− =/ page=(unit ischeme) (find-jibb-mold %page u.prelude)
14504− =/ main=(unit ischeme) (ienv-lookup %main env)
14506− ?. ?=(~ vars.u.main) |
14507− ?. ?=(~ (itype-vars typ.u.main)) |
14508− =/ instance=[typ=itype state=istate] (instantiate-scheme u.page *istate)
14509− =/ main-fit=ifit (direct-invariant typ.u.main typ.instance ~ next.state.instance)
14510− ?. ?=(%ok -.main-fit) |
14511− (page-load-derived load.parts ds imports graph u.prelude)
14513−++ program-main-closed
14514− |= [parts=[init=term update=term view=term subs=term] ds=(list def) env=ienv prelude=(unit ifile) imports=ijimports graph=irequest-graph]
14517− ?~ (ienv-lookup %program values.u.prelude) |
14518− =/ program=(unit ischeme) (find-jibb-mold %program u.prelude)
14520− =/ main=(unit ischeme) (ienv-lookup %main env)
14522− ?. ?=(~ vars.u.main) |
14523− ?. ?=(~ (itype-vars typ.u.main)) |
14524− =/ instance=[typ=itype state=istate] (instantiate-scheme u.program *istate)
14525− =/ main-fit=ifit (direct-invariant typ.u.main typ.instance ~ next.state.instance)
14526− ?. ?=(%ok -.main-fit) |
14527− =/ init=(unit ischeme) (ienv-lookup init.parts env)
14529− ?. ?=(~ vars.u.init) |
14530− ?. ?=(%fn -.typ.u.init) |
14531− ?. ?=(~ (itype-vars sample.typ.u.init)) |
14532− ?. ?=(~ (itype-vars product.typ.u.init)) |
14533− =/ data=igate-free (gate-free-type sample.typ.u.init 256 ~)
14534− ?. =(%yes verdict.data) |
14535− =/ model=igate-free (gate-free-type product.typ.u.init left.data ~)
14536− ?. =(%yes verdict.model) |
14537− =/ subs=(list def)
14538− (skim ds |=(d=def &(?=(%value -.d) =(subs.parts name.d))))
14539− ?. ?=([* ~] subs) |
14540− |((program-subs-empty i.subs) (program-subs-watch i.subs imports graph u.prelude))
14542−:: The two outer sample faces are binder names, not part of the action/state
14543−:: relation. Leave every face inside either component untouched.
14544−++ store-update-unfaced
14547− ?. ?=(%fn -.typ) typ
14548− ?. ?=(%cell -.sample.typ) typ
14549− =/ head=itype hed.sample.typ
14550− =/ tail=itype tal.sample.typ
14551− =? head ?=(%face -.head) body.head
14552− =? tail ?=(%face -.tail) body.tail
14553− typ(sample [%cell head tail])
14555−:: The builder erases the action from main. Recover it only from the local
14556−:: poke mold and check both ordinary components invariantly.
14557−++ store-main-closed
14558− |= [parts=[init=term update=term] action=term env=ienv molds=imold-types prelude=(unit ifile)]
14561− =/ builder=(unit ischeme) (ienv-lookup %store values.u.prelude)
14563− ?. ?=([@ @ ~] vars.u.builder) ~
14564− =/ state-var=@ud i.vars.u.builder
14565− =/ action-var=@ud i.t.vars.u.builder
14566− ?: =(state-var action-var) ~
14567− =/ builder-sample=itype
14568− [%cell [%face %init [%var state-var]] [%face %update [%fn [%cell [%var action-var] [%var state-var]] [%var state-var]]]]
14569− =/ builder-product=itype [%cell [%face %init [%var state-var]] [%face %update [%noun ~]]]
14570− ?. =(typ.u.builder [%fn builder-sample builder-product]) ~
14571− =/ store=(unit ischeme) (find-jibb-mold %store u.prelude)
14573− ?. ?=([@ ~] vars.u.store) ~
14574− ?. =(typ.u.store [%cell [%face %init [%var i.vars.u.store]] [%face %update [%noun ~]]]) ~
14575− =/ state=(unit ischeme) (find-jibb-mold %state [~ molds /tmp ~ ~ ~ ~ ~])
14577− =/ action-mold=(unit ischeme) (find-jibb-mold action [~ molds /tmp ~ ~ ~ ~ ~])
14579− ?. &(?=(~ vars.u.state) ?=(~ (itype-vars typ.u.state))) ~
14580− ?. &(?=(~ vars.u.action-mold) ?=(~ (itype-vars typ.u.action-mold))) ~
14581− =/ canonical=(unit itype) (template-apply u.store ~[typ.u.state])
14583− =/ main=(unit ischeme) (ienv-lookup %main env)
14584− =/ main-fit=(unit ifit)
14585− ?~(main ~ `(direct-invariant typ.u.main u.canonical ~ 0))
14588− ?. ?=(~ vars.u.main) |
14589− ?. ?=(~ (itype-vars typ.u.main)) |
14591− ?=(%ok -.u.main-fit)
14593− =/ init=(unit ischeme) (ienv-lookup init.parts env)
14595− ?. ?=(~ vars.u.init) ~
14596− ?. ?=(~ (itype-vars typ.u.init)) ~
14597− =/ init-fit=ifit (direct-invariant typ.u.init typ.u.state ~ 0)
14598− ?. ?=(%ok -.init-fit) ~
14599− =/ update=(unit ischeme) (ienv-lookup update.parts env)
14601− ?. ?=(~ vars.u.update) ~
14602− ?. ?=(~ (itype-vars typ.u.update)) ~
14603− =/ expected=itype [%fn [%cell typ.u.action-mold typ.u.state] typ.u.state]
14604− =/ update-fit=ifit (direct-invariant (store-update-unfaced typ.u.update) expected ~ 0)
14605− ?. ?=(%ok -.update-fit) ~
14608++ infer-jibb-file
12390++ infer-jibb-file
14609 |= [at=path src=@t externals=iexternals mark-externals=imark-externals modules=jbundle active=(list path) prelude-values=(list term) prelude-molds=(list term) cache=jcache prelude=(unit ifile)]
12391 |= [at=path src=@t externals=iexternals mark-externals=imark-externals modules=jbundle active=(list path) prelude-values=(list term) prelude-molds=(list term) cache=jcache prelude=(unit ifile)]
14610 ^- jfile-result
12392 ^- jfile-result
14611− =/ out=jfile-detailed-result
14612− (infer-jibb-file-detailed at src externals mark-externals modules active prelude-values prelude-molds cache prelude)
14613− ?: ?=(%| -.out) [%| message.p.out]
14615−:: Returns structured root-source overlap evidence after the same full check.
14616−++ infer-jibb-file-detailed
14617− |= [at=path src=@t externals=iexternals mark-externals=imark-externals modules=jbundle active=(list path) prelude-values=(list term) prelude-molds=(list term) cache=jcache prelude=(unit ifile)]
14618− ^- jfile-detailed-result
14619 =/ parsed (parse at src)
12393 =/ parsed (parse at src)
14620− ?: ?=(%| -.parsed) [%| [(crip "module source does not parse: {(spud at)}") ~]]
12394+ ?: ?=(%| -.parsed) [%| (crip "module source does not parse: {(spud at)}")]
14621 =/ mod=module p.parsed
12395 =/ mod=module p.parsed
14622 =/ duplicate=(unit idiag) (duplicate-defs defs.mod)
12396 =/ duplicate=(unit idiag) (duplicate-defs defs.mod)
14623− ?^ duplicate [%| [(show-duplicate-fields at src u.duplicate) ~]]
12397+ ?^ duplicate [%| (show-duplicate-fields at src u.duplicate)]
14624− ?: &(?=([%ui %api *] at) ?=(^ (program-main-def defs.mod)))
14625− [%| [(crip "module kind needs unsupported inference: {(spud at)}") ~]]
14626 ?: ?=([%ui %api *] at)
12398 ?: ?=([%ui %api *] at)
14627− =/ poke=(each ifile @t)
14628− (api-poke-interface-result at mod mark-externals prelude-values prelude-molds prelude)
12399+ =/ iface=(unit ifile) (api-poke-interface at mod mark-externals prelude-values prelude-molds prelude)
14630− =/ iface=ifile p.poke
12400+ ?^ iface
14631− =/ checked=ifile iface(source `src, graph `[(silt `(list path)`~[at]) ~ ~ modules prelude prelude-values prelude-molds externals mark-externals])
12401+ =/ checked=ifile u.iface(source `src, graph `[(silt `(list path)`~[at]) ~ modules prelude prelude-values prelude-molds externals mark-externals])
14632 [%& [checked [[at checked] cache]]]
12402 [%& [checked [[at checked] cache]]]
14633− :: A clashing derived name is an error wherever the checks below stop.
14634− =/ clash=(unit idiag)
14635− ?. ?=([%ui %api @ %jibb ~] at) ~
14636− (api-derived-clash mod prelude-values)
14637− ?^ clash [%| [(show-duplicate-fields at src u.clash) ~]]
14638− :: So is a name conflict in its scope, reported as for other modules.
14639− :: `+$ paths` and `+$ poke` are declarations, not molds (overview), and
14640− :: a `/%` mark names a mold, so it conflicts only with another mark or
14641− :: mold: `/% %todos` beside the request `todos` is the usual API.
14642− =/ ordinary=(list def)
14643− (skim defs.mod |=(d=def !&(?=(%mold -.d) |(=(%paths name.d) =(%poke name.d)))))
14644− =/ marks=(list term) (collect-mark-imports imports.mod)
14645− =/ mold-names=(list term)
14646− (turn (collect-simple-molds ordinary) |=(m=[name=term body=shape] name.m))
14647− =/ faces=(list import) (skip imports.mod |=(i=import ?=(%mark -.i)))
14648− ?. ?& (module-scope-valid mod(defs ordinary, imports faces) prelude-values prelude-molds)
14651− ?& (unique-value-name n marks)
14652− !(lien mold-names |=(m=term =(m n)))
14653− !(lien prelude-molds |=(m=term =(m n)))
14656− [%| [(crip "module has conflicting names: {(spud at)}") ~]]
14657− ?~ prelude [%| [(crip "API module needs unsupported inference: {(spud at)}") ~]]
12403+ ?~ prelude [%| (crip "API module needs unsupported inference: {(spud at)}")]
14658 =/ prepared=iprelude [u.prelude prelude-values prelude-molds]
12404 =/ prepared=iprelude [u.prelude prelude-values prelude-molds]
14659− :: A failing Jibb import gives its own error, which may be definite, as
14660− :: it does for other modules; the constructors below would only wrap it.
14661− :: They resolve the same imports again, from the interfaces cached here.
14662− =/ js=jimports-detailed-result
14663− (resolve-jibb-imports-detailed imports.mod externals mark-externals modules active prelude-values prelude-molds cache prelude)
14664− ?: ?=(%| -.js) [%| p.js]
14665− :: Without `+$ paths` only the poke-only interface applies; keep its reason.
14666− ?. (lien defs.mod |=(d=def &(?=(%mold -.d) =(%paths name.d))))
14667− [%| [(crip "API module needs unsupported inference: {(spud at)}: {(trip p.poke)}") ~]]
14668− :: Each constructor names the part that stopped it; keep that reason.
14669 =/ narrow=?
12405 =/ narrow=?
14670 ?. ?=([[%mark *] ~] imports.mod) |
12406 ?. ?=([[%mark *] ~] imports.mod) |
14671 ?. ?=([[%mold *] ~] defs.mod) |
12407 ?. ?=([[%mold *] ~] defs.mod) |
@@ -14673,41 +12409,26 @@
14673 !?=(%union -.shape.i.defs.mod)
12409 !?=(%union -.shape.i.defs.mod)
14674 ?: narrow
12410 ?: narrow
14675 =/ request=(each ione-request-interface @t)
12411 =/ request=(each ione-request-interface @t)
14676− (one-request-interface-graph at src externals mark-externals modules active cache.p.js `prepared)
12412+ (one-request-interface-graph at src externals mark-externals modules active cache `prepared)
14677− ?: ?=(%| -.request) [%| [(crip "API module needs unsupported inference: {(spud at)}: {(trip p.request)}") ~]]
12413+ ?: ?=(%| -.request) [%| (crip "API module needs unsupported inference: {(spud at)}")]
14678 =/ checked=ifile iface.p.request
12414 =/ checked=ifile iface.p.request
14679 [%& [checked [[at checked] dependencies.paths.support.p.request]]]
12415 [%& [checked [[at checked] dependencies.paths.support.p.request]]]
14680 =/ multi=(each [iface=ifile cache=jcache] @t)
12416 =/ multi=(each [iface=ifile cache=jcache] @t)
14681− (multi-request-interface-graph at src externals mark-externals modules active cache.p.js `prepared)
12417+ (multi-request-interface-graph at src externals mark-externals modules active cache `prepared)
14682− ?: ?=(%| -.multi) [%| [(crip "API module needs unsupported inference: {(spud at)}: {(trip p.multi)}") ~]]
12418+ ?: ?=(%| -.multi) [%| (crip "API module needs unsupported inference: {(spud at)}")]
14683 [%& [iface.p.multi [[at iface.p.multi] cache.p.multi]]]
12419 [%& [iface.p.multi [[at iface.p.multi] cache.p.multi]]]
14684− =/ main=(unit def) (program-main-def defs.mod)
14685− =/ main-parts=(unit [init=term update=term view=term subs=term])
14686− ?~(main ~ (program-main-parts u.main))
14687− =/ page-parts=(unit [load=term view=term])
14688− ?~(main ~ (page-main-parts u.main))
14689− =/ store-parts=(unit [init=term update=term])
14690− ?~(main ~ (store-main-parts u.main))
14691− =/ declaration=(each istore-declaration (unit idiag))
14692− ?~(store-parts [%| ~] (store-declaration mod prelude-values prelude-molds))
14693− =/ clash=(unit idiag) ?:(?=(%| -.declaration) p.declaration ~)
14694− ?^ clash [%| [(show-duplicate-fields at src u.clash) ~]]
14695− =/ declared=(unit istore-declaration)
14696− ?:(?=(%| -.declaration) ~ `p.declaration)
14697− ?: &(?=(^ store-parts) ?=(~ declared))
14698− [%| [(crip "module kind or scope needs unsupported inference: {(spud at)}") ~]]
14699− ?: &(?=([%ui %stores *] at) ?=(^ main) ?=(~ store-parts))
14700− [%| [(crip "module kind needs unsupported inference: {(spud at)}") ~]]
14701− =/ ds=(list def) ?~(declared defs.mod defs.u.declared)
14702− =/ checking=module mod(defs ds)
14703− ?. (module-scope-valid checking prelude-values prelude-molds)
12420+ ?. (module-scope-valid mod prelude-values prelude-molds)
12421+ ?: (pending-declared-poke at mod prelude-values prelude-molds)
12422+ [%| (crip "module kind or scope needs unsupported inference: {(spud at)}")]
14704− [%| [(crip "module has conflicting names: {(spud at)}") ~]]
12423+ [%| (crip "module has conflicting names: {(spud at)}")]
14705− =/ vals=(list term) (global-value-names ds)
12424+ =/ vals=(list term) (global-value-names defs.mod)
12425+ ?: (lien vals |=(n=term =(n %main)))
12426+ [%| (crip "module kind needs unsupported inference: {(spud at)}")]
14706− =/ js=jimports-detailed-result (resolve-jibb-imports-detailed imports.mod externals mark-externals modules active prelude-values prelude-molds cache prelude)
12427+ =/ js=jimports-result (resolve-jibb-imports imports.mod externals mark-externals modules active prelude-values prelude-molds cache prelude)
14707 ?: ?=(%| -.js) [%| p.js]
12428 ?: ?=(%| -.js) [%| p.js]
14708 =/ collected=grec-collected
12429 =/ collected=grec-collected
14709− ?^ imports.mod [(collect-simple-molds ds) *(map term shape)]
12430+ ?^ imports.mod [(collect-simple-molds defs.mod) *(map term shape)]
14710− (grec-collect-molds ds)
12431+ (grec-collect-molds defs.mod)
14711 =/ molds=imolds molds.collected
12432 =/ molds=imolds molds.collected
14712 =/ globals=(list term) (weld prelude-values (weld (import-binding-names imports.mod) vals))
12433 =/ globals=(list term) (weld prelude-values (weld (import-binding-names imports.mod) vals))
14713 =/ surs=(list term) (collect-sur-imports imports.mod)
12434 =/ surs=(list term) (collect-sur-imports imports.mod)
@@ -14728,114 +12449,28 @@
14728 ?: (lien molds |=(m=[name=term body=shape] =(%list name.m))) ~
12449 ?: (lien molds |=(m=[name=term body=shape] =(%list name.m))) ~
14729 `[at src u.prelude index]
12450 `[at src u.prelude index]
14730 =. grec-index.state index
12451 =. grec-index.state index
14731− =/ mts=(each imold-types imold-failure) (module-mold-types-detail molds state)
12452+ =/ mts=(each imold-types @t) (module-mold-types molds state)
14733− ?~ overlap.p.mts [%| [(crip "{(trip message.p.mts)}: {(spud at)}") ~]]
12453+ ?: ?=(%| -.mts) [%| (crip "{(trip p.mts)}: {(spud at)}")]
14734− =/ witness=[name=term cases=upair] u.overlap.p.mts
14735− =/ first=@t (show-error src [at line.beg.first.cases.witness col.beg.first.cases.witness "first union case"])
14736− =/ second=@t (show-error src [at line.beg.second.cases.witness col.beg.second.cases.witness "overlapping case"])
14737− =/ msg=@t (of-wain:format ~[(crip "module mold {(trip name.witness)} has overlapping cases") first second])
14738− [%| [msg `[at src name.witness cases.witness]]]
14739 =/ resolution=iresolved
12454 =/ resolution=iresolved
14740 ?~ index
12455 ?~ index
14741− (resolve-groups ds molds globals externals surs mark-externals marks resolved.p.js reserved at prelude)
12456+ (resolve-groups defs.mod molds globals externals surs mark-externals marks resolved.p.js reserved at prelude)
14742− (resolve-groups-core ds molds globals externals surs mark-externals marks resolved.p.js reserved at prelude index)
12457+ (resolve-groups-core defs.mod molds globals externals surs mark-externals marks resolved.p.js reserved at prelude index)
14743 =/ env=ienv env.resolution
12458 =/ env=ienv env.resolution
14744− =/ recovered=iresolved
14745− ?~ main resolution
14746− ?~ main-parts resolution
14747− =/ updated=(unit iresolved)
14748− (program-update-context u.main u.main-parts ds resolution state)
14749− =/ with-update=iresolved ?~(updated resolution u.updated)
14750− =/ subscribed=(unit iresolved)
14751− (program-subs-context u.main-parts ds with-update state)
14752− =/ with-subs=iresolved ?~(subscribed with-update u.subscribed)
14753− =/ viewed=(unit iresolved)
14754− (program-view-context u.main-parts ds with-subs state)
14755− =/ with-keyed-view=iresolved ?~(viewed with-subs u.viewed)
14756− =/ plain-view=(unit iresolved)
14757− ?^(viewed ~ (program-plain-view-context u.main-parts ds with-keyed-view state))
14758− =/ with-view=iresolved ?~(plain-view with-keyed-view u.plain-view)
14759− =/ initialized=(unit iresolved)
14760− (program-init-context u.main u.main-parts ds with-view state)
14761− =/ with-initialized=iresolved ?~(initialized with-view u.initialized)
14762− =/ plain-init=(unit iresolved)
14763− ?^(initialized ~ (program-plain-init-context u.main-parts ds with-initialized state))
14764− =/ components=iresolved ?~(plain-init with-initialized u.plain-init)
14765− (program-main-context u.main ds components state)
14766− =. env env.recovered
14767− =. artifacts.resolution artifacts.recovered
14769− ?: (module-values-complete ds env) env
12460+ ?: (module-values-complete defs.mod env) env
14770 ?: |(?=([%ui %stores *] at) ?=(^ imports.mod) ?=(^ prelude) ?=(^ prelude-values) ?=(^ prelude-molds)) env
12461 ?: |(?=([%ui %stores *] at) ?=(^ imports.mod) ?=(^ prelude) ?=(^ prelude-values) ?=(^ prelude-molds)) env
14771 ?: (gth (met 3 src) 65.536) env
12462 ?: (gth (met 3 src) 65.536) env
14772− ?: (gth (lent ds) 64) env
12463+ ?: (gth (lent defs.mod) 64) env
14773− ?. (dg-source-candidate ds 64) env
12464+ ?. (dg-source-candidate defs.mod 64) env
14774 =/ transaction=(unit dgcommit) (dg-root-source at src)
12465 =/ transaction=(unit dgcommit) (dg-root-source at src)
14775 ?~ transaction env
12466 ?~ transaction env
14776 ?: (dg-interface-safe env.u.transaction) env.u.transaction
12467 ?: (dg-interface-safe env.u.transaction) env.u.transaction
14778− =/ required=(list def)
14780− (skim ds |=(d=def !&(?=(%value -.d) =(%main name.d))))
14781− ?. (module-values-complete required env)
12469+ ?. (module-values-complete defs.mod env)
14782− =/ pending=(unit [at=span msg=tape]) (module-pending-tag required env state 64)
14784− [%| [(show-error src [at line.beg.at.u.pending col.beg.at.u.pending msg.u.pending]) ~]]
14785− :: A shadowing sample is an error, so it comes before any named value.
14786− =/ values=(list term) (weld prelude-values (weld (api-import-faces imports.mod) vals))
14787− =/ shadow=(unit [name=term at=span]) (module-sample-shadow required env values)
14789− =/ msg=tape "sample `{(trip name.u.shadow)}` shadows a name already in scope"
14790− [%| [(show-error src [at line.beg.at.u.shadow col.beg.at.u.shadow msg]) ~]]
14791− =/ missing=(unit term) (module-missing-value required env)
14792− =/ named=tape ?~(missing "" ": ++ {(trip u.missing)}")
14793− [%| [(crip "module definitions need unsupported inference: {(spud at)}{named}") ~]]
12470+ [%| (crip "module definitions need unsupported inference: {(spud at)}")]
14794− =/ initial=irequest-graph [(silt `(list path)`~[at]) ~ ~ modules prelude prelude-values prelude-molds externals mark-externals]
12471+ =/ initial=irequest-graph [(silt `(list path)`~[at]) ~ modules prelude prelude-values prelude-molds externals mark-externals]
14795 =/ graph=(unit irequest-graph) (request-graph-merge resolved.p.js initial (add 1 (lent resolved.p.js)))
12472 =/ graph=(unit irequest-graph) (request-graph-merge resolved.p.js initial (add 1 (lent resolved.p.js)))
14796− ?~ graph [%| ['module request evidence needs unsupported inference' ~]]
12473+ ?~ graph [%| 'module request evidence needs unsupported inference']
14797− =/ static-main=(unit ischeme)
14802− (static-main-specialized env prelude)
14803− =? env ?=(^ static-main)
14804− [[%main u.static-main] (skim env |=(entry=[name=term scheme=ischeme] !=(%main name.entry)))]
14805− =/ store-main=(unit ischeme)
14808− (store-main-closed u.store-parts action.u.declared env p.mts prelude)
14809− =? env ?=(^ store-main)
14810− [[%main u.store-main] (skim env |=(entry=[name=term scheme=ischeme] !=(%main name.entry)))]
14813− ?^ main-parts (program-main-closed u.main-parts ds env prelude resolved.p.js u.graph)
14814− ?^ page-parts (page-main-closed u.page-parts ds env prelude resolved.p.js u.graph)
14815− ?^ store-parts ?=(^ store-main)
14818− [%| [(crip "module kind needs unsupported inference: {(spud at)}") ~]]
14819− =/ store-derived=(unit [values=ienv evidence=istore-request-evidence])
14822− =/ state=(unit ischeme) (find-jibb-mold %state [~ p.mts at ~ ~ ~ ~ ~])
14824− =/ action-mold=(unit ischeme) (find-jibb-mold action.u.declared [~ p.mts at ~ ~ ~ ~ ~])
14826− =/ schemes=(unit [state=ischeme action=ischeme])
14827− (store-derived-schemes u.prelude prelude-values prelude-molds typ.u.state typ.u.action-mold)
14829− =/ evidence=istore-request-evidence
14830− [at src typ.u.state action.u.declared typ.u.action-mold]
14831− `[~[[%state state.u.schemes] [action.u.declared action.u.schemes]] evidence]
14832− ?: &(?=(^ declared) ?=(~ store-derived))
14833− [%| [(crip "store derived gates need unsupported inference: {(spud at)}") ~]]
14834− =? env ?=(^ store-derived) (weld values.u.store-derived env)
14835− =? graph ?=(^ store-derived)
14836− `u.graph(stores [evidence.u.store-derived stores.u.graph])
14837− ?. (request-graph-bounded u.graph)
14838− [%| ['module request evidence needs unsupported inference' ~]]
14839 =/ iface=ifile [env p.mts at ~ artifacts.resolution ~ `src graph]
12474 =/ iface=ifile [env p.mts at ~ artifacts.resolution ~ `src graph]
14840 [%& [iface [[at iface] cache.p.js]]]
12475 [%& [iface [[at iface] cache.p.js]]]
@@ -14945,13 +12580,15 @@
14945 =/ prelude-molds=(list term) molds.u.prepared
12580 =/ prelude-molds=(list term) molds.u.prepared
14946 =/ iface=(unit ifile) `iface.u.prepared
12581 =/ iface=(unit ifile) `iface.u.prepared
14947 ?. (module-scope-valid p.parsed prelude-values prelude-molds)
12582 ?. (module-scope-valid p.parsed prelude-values prelude-molds)
12583+ ?: (pending-declared-poke file p.parsed prelude-values prelude-molds)
12584+ 'partial inference; module not checked\0amodule kind or scope needs unsupported inference'
14948 'partial inference; module not checked\0amodule has conflicting names'
12585 'partial inference; module not checked\0amodule has conflicting names'
14949 =/ js=jimports-result
12586 =/ js=jimports-result
14950 (resolve-jibb-imports imports.p.parsed externals mark-externals modules ~[file] prelude-values prelude-molds ~ iface)
12587 (resolve-jibb-imports imports.p.parsed externals mark-externals modules ~[file] prelude-values prelude-molds ~ iface)
14951 ?: ?=(%| -.js) (of-wain:format ~['partial inference; module not checked' p.js])
12588 ?: ?=(%| -.js) (of-wain:format ~['partial inference; module not checked' p.js])
14952 =/ scope-values=(list term)
12589 =/ scope-values=(list term)
14953 (weld prelude-values (weld (collect-sur-imports imports.p.parsed) (collect-mark-imports imports.p.parsed)))
12590 (weld prelude-values (weld (collect-sur-imports imports.p.parsed) (collect-mark-imports imports.p.parsed)))
14954− (golden-types-in-context-core file src externals mark-externals resolved.p.js scope-values prelude-molds iface prepared)
12591+ (golden-types-in-context file src externals mark-externals resolved.p.js scope-values prelude-molds iface)
14956:: +golden-types-with-marks: supply declared mark types separately from /sur
12593:: +golden-types-with-marks: supply declared mark types separately from /sur
14957:: entries, as [mark result] with the result from +read-mark:jibb-import.
12594:: entries, as [mark result] with the result from +read-mark:jibb-import.
@@ -14982,10 +12619,6 @@
14982++ golden-types-in-context
12619++ golden-types-in-context
14983 |= [file=path src=@t externals=iexternals mark-externals=imark-externals jimports=ijimports prelude-values=(list term) reserved-molds=(list term) prelude=(unit ifile)]
12620 |= [file=path src=@t externals=iexternals mark-externals=imark-externals jimports=ijimports prelude-values=(list term) reserved-molds=(list term) prelude=(unit ifile)]
14985− (golden-types-in-context-core file src externals mark-externals jimports prelude-values reserved-molds prelude ~)
14986−++ golden-types-in-context-core
14987− |= [file=path src=@t externals=iexternals mark-externals=imark-externals jimports=ijimports prelude-values=(list term) reserved-molds=(list term) prelude=(unit ifile) prepared=(unit iprelude)]
14989 =. reserved-molds (weld reserved-molds (turn jimports |=(j=[face=term interface=ifile] face.j)))
12622 =. reserved-molds (weld reserved-molds (turn jimports |=(j=[face=term interface=ifile] face.j)))
14990 =/ parsed (parse file src)
12623 =/ parsed (parse file src)
14991 ?: ?=(%| -.parsed) (show-error src p.parsed)
12624 ?: ?=(%| -.parsed) (show-error src p.parsed)
@@ -15005,27 +12638,19 @@
15005 =/ eligible=?
12638 =/ eligible=?
15006 ?& ?=(~ imports.p.parsed)
12639 ?& ?=(~ imports.p.parsed)
15007 ?=(~ jimports)
12640 ?=(~ jimports)
12642+ ?=(~ prelude-values)
12643+ ?=(~ reserved-molds)
15008 !?=([%ui %api *] file)
12644 !?=([%ui %api *] file)
15009 !?=([%ui %stores *] file)
12645 !?=([%ui %stores *] file)
15010 !(lien (global-value-names ds) |=(n=term =(n %main)))
12646 !(lien (global-value-names ds) |=(n=term =(n %main)))
12647+ (module-scope-valid p.parsed ~ ~)
15011 !(module-values-complete ds env)
12648 !(module-values-complete ds env)
15012 (lte (met 3 src) 65.536)
12649 (lte (met 3 src) 65.536)
15013 (lte (lent ds) 64)
12650 (lte (lent ds) 64)
15014− ?| &(?=(~ prepared) ?=(~ prelude) ?=(~ prelude-values) ?=(~ reserved-molds) (module-scope-valid p.parsed ~ ~) (dg-source-candidate ds 64))
12651+ (dg-source-candidate ds 64)
15017− =(u.prelude iface.u.prepared)
15018− =(prelude-values values.u.prepared)
15019− =(reserved-molds molds.u.prepared)
15020− (module-scope-valid p.parsed values.u.prepared molds.u.prepared)
15021− (dg-prepared-candidate ds 64)
15025− =/ transaction=(unit dgcommit)
12653+ =/ transaction=(unit dgcommit) ?:(eligible (dg-root-source file src) ~)
15027− ?~ prepared (dg-root-source file src)
15028− (dg-root-prepared file src u.prepared)
15029 =. recovered
12654 =. recovered
15030 ?~ transaction ~
12655 ?~ transaction ~
15031 ?. &((module-values-complete ds env.u.transaction) (dg-interface-safe env.u.transaction)) ~
12656 ?. &((module-values-complete ds env.u.transaction) (dg-interface-safe env.u.transaction)) ~
@@ -15117,7 +12742,7 @@
15117 ?: =(0 fuel) ~
12742 ?: =(0 fuel) ~
15118 =. fuel (dec fuel)
12743 =. fuel (dec fuel)
15119 =/ t=itype i.todo
12744 =/ t=itype i.todo
15120− ?: ?=(?(%var %fvar %avar %rvar %nvar %rnvar %tag) -.t)
12745+ ?: ?=(?(%var %avar %rvar %nvar %rnvar %tag) -.t)
15121 =/ node-id=@ud ?:(?=(%tag -.t) id.t +.t)
12746 =/ node-id=@ud ?:(?=(%tag -.t) id.t +.t)
15122 =/ found=(unit itype) (itype-lookup node-id sub)
12747 =/ found=(unit itype) (itype-lookup node-id sub)
15123 ?~ found $(todo t.todo, ids [node-id ids])
12748 ?~ found $(todo t.todo, ids [node-id ids])
@@ -15311,31 +12936,6 @@
15311 [%& result st(next +(next.st), obligations [ex ey obligations.st])]
12936 [%& result st(next +(next.st), obligations [ex ey obligations.st])]
15312 [%& typ.p.left state.p.right]
12937 [%& typ.p.left state.p.right]
15314−:: A direct tuple literal may wait for a later exact result context.
15315−:: Each pending literal retains its source tag and its own fit obligation.
15316−++ dg-infer-tuple-items
15317− |= [items=(list item) env=ienv state=istate]
15319− ?~ items [%| ["empty cell is not supported by partial inference" ~]]
15320− =/ head=iresult (infer-fragment val.i.items env state)
15321− ?: ?=(%| -.head) head
15322− =/ typ=itype typ.p.head
15323− =/ st=istate state.p.head
15324− =/ adjusted=(unit [typ=itype state=istate])
15325− ?. (dg-owned-arm-literal val.i.items typ tags.st sub.st next.state) `[typ st]
15326− ?: (gth (lent obligations.st) 63) ~
15327− =/ pending=itype [%var next.st]
15328− =/ edge=dgo [typ pending (span-of val.i.items) at.i.items]
15329− `[pending st(next +(next.st), obligations [edge obligations.st])]
15330− ?~ adjusted [%| ["deferred tuple context needs unsupported inference" ~]]
15331− =. typ typ.u.adjusted
15332− =. st state.u.adjusted
15333− =. typ ?~(face.i.items typ [%face u.face.i.items typ])
15334− ?~ t.items [%& typ st]
15335− =/ tail=iresult $(items t.items, state st)
15336− ?: ?=(%| -.tail) tail
15337− [%& [%cell typ typ.p.tail] state.p.tail]
15339:: Deferred inference uses only source forms whose successful fit sites are
12939:: Deferred inference uses only source forms whose successful fit sites are
15340:: guarded below; a shared source-node budget bounds this screen.
12940:: guarded below; a shared source-node budget bounds this screen.
15341++ dg-safe-expressions
12941++ dg-safe-expressions
@@ -15345,13 +12945,6 @@
15345 =/ first=(unit @ud) (dg-safe-expression i.todo fuel)
12945 =/ first=(unit @ud) (dg-safe-expression i.todo fuel)
15346 ?~ first ~
12946 ?~ first ~
15347 $(todo t.todo, fuel u.first)
12947 $(todo t.todo, fuel u.first)
15349− |= [items=(list item) fuel=@ud]
15352− =/ first=(unit @ud) (dg-safe-expression val.i.items fuel)
15354− $(items t.items, fuel u.first)
15355++ dg-safe-expression
12948++ dg-safe-expression
15356 |= [e=expr fuel=@ud]
12949 |= [e=expr fuel=@ud]
15357 ^- (unit @ud)
12950 ^- (unit @ud)
@@ -15369,7 +12962,6 @@
15369 $(e final.e, fuel fuel)
12962 $(e final.e, fuel fuel)
15370 %gate $(e body.e, fuel fuel)
12963 %gate $(e body.e, fuel fuel)
15371 %gate-wide $(e body.e, fuel fuel)
12964 %gate-wide $(e body.e, fuel fuel)
15372− %tuple (dg-safe-items items.e fuel)
15373 %branch
12965 %branch
15374 ?. (dg-boolean-patterns e) ~
12966 ?. (dg-boolean-patterns e) ~
15375 ?> ?=(^ arms.e)
12967 ?> ?=(^ arms.e)
@@ -15509,28 +13101,6 @@
15509 ?: (dg-direct-source val.i.ds 64) &
13101 ?: (dg-direct-source val.i.ds 64) &
15510 $(ds t.ds, fuel (dec fuel))
13102 $(ds t.ds, fuel (dec fuel))
15512−++ dg-prepared-source
15513− |= [e=expr fuel=@ud]
15515− ?: (dg-direct-source e fuel) &
15518− %group $(e inner.e, fuel (dec fuel))
15519− %gate $(e body.e, fuel (dec fuel))
15520− %gate-wide $(e body.e, fuel (dec fuel))
15521− %cast $(e val.e, fuel (dec fuel))
15522− %body ?~(defs.e $(e final.e, fuel (dec fuel)) |)
15525−++ dg-prepared-candidate
15526− |= [ds=(list def) fuel=@ud]
15530− ?. ?=(%value -.i.ds) $(ds t.ds, fuel (dec fuel))
15531− ?: (dg-prepared-source val.i.ds 64) &
15532− $(ds t.ds, fuel (dec fuel))
15534++ dg-interface-safe
13104++ dg-interface-safe
15535 |= [env=ienv]
13105 |= [env=ienv]
@@ -15576,47 +13146,6 @@
15576 (dg-stage defs base base st ~ 64)
13146 (dg-stage defs base base st ~ 64)
15578 [& (transact)]
13148 [& (transact)]
15579−:: The caller supplies the trusted prepared prelude. This transaction is
15580−:: only report evidence; the ordinary module resolver does not publish it.
15581−++ dg-root-prepared
15582− |= [at=path src=@t prepared=iprelude]
15583− ^- (unit dgcommit)
15584− ?: ?=([%ui %api *] at) ~
15585− ?: ?=([%ui %stores *] at) ~
15586− ?: (gth (met 3 src) 65.536) ~
15587− =/ parsed (parse at src)
15588− ?: ?=(%| -.parsed) ~
15589− ?^ imports.p.parsed ~
15590− ?. (module-scope-valid p.parsed values.prepared molds.prepared) ~
15591− ?^ (duplicate-defs defs.p.parsed) ~
15592− =/ defs=(list def) defs.p.parsed
15593− ?: (gth (lent defs) 64) ~
15594− ?: (lien (global-value-names defs) |=(n=term =(n %main))) ~
15595− ?. (dg-prepared-candidate defs 64) ~
15596− =/ local-molds=imolds (collect-simple-molds defs)
15597− =/ globals=(list term) (weld values.prepared (global-value-names defs))
15598− =/ iface=ifile iface.prepared
15599− =/ prelude=(unit ifile) `iface
15600− =/ resolution=iresolved
15601− (resolve-groups defs local-molds globals ~ ~ ~ ~ ~ molds.prepared at prelude)
15602− ?^ grouped.resolution ~
15603− ?^ artifacts.resolution ~
15604− =/ base=ienv env.resolution
15606− (turn molds.iface |=(x=[name=term template=ischeme] [name.x template.x]))
15607− =/ all-env=ienv (weld base (weld values.iface templates))
15608− =/ free=(unit dgscan) (dg-env all-env ~ 32.768 ~)
15611− =/ all=(unit dgscan) (dg-all-env-ids all-env 32.768 ~)
15613− =/ fresh=@ud (dg-next-id ids.u.all 0)
15614− =/ st=istate *istate
15615− =. st st(next fresh, defer `~, molds local-molds, globals globals, at at, reserved-molds molds.prepared, prelude prelude, top-molds (turn local-molds |=(m=[name=term body=shape] name.m)), in-mold |, jrec-fuel 256)
15616− =/ checked-molds=(each imold-types @t) (module-mold-types local-molds st)
15617− ?: ?=(%| -.checked-molds) ~
15618− (dg-stage defs base base st ~ 64)
15620++ dg-all-env-ids
13149++ dg-all-env-ids
15621 |= [env=ienv fuel=@ud ids=(list @ud)]
13150 |= [env=ienv fuel=@ud ids=(list @ud)]
15622 ^- (unit dgscan)
13151 ^- (unit dgscan)