1	import Base
2	import bundle_pack.bend as B
3	
4	# Experimental reversible constructor RESULT receipts, not a universal Raw->C
5	# inverse or production Decode policy. Only the trusted author supplies undo.
6	type Construction<Raw:Type,Cooked:Type,Error:Data> is Type:
7	  Constructed{cooked:Cooked,undo:Cooked -> Raw}
8	  Invalid{raw:Raw,error:Error}
9	type Staged<Context:Type,Raw:Type,Cooked:Type,Error:Data> is Type:
10	  Valid{context:Context,cooked:Cooked,undo:Cooked -> Raw,positions:List<&2,Maybe<&2,Error>>}
11	  Failed{context:Context,raw:Raw,positions:List<&2,Maybe<&2,Error>>}
12	def undo_pack(~HR:Type,~HC:Type,~TR:Type,~TC:Type,headUndo:HC -> HR,tailUndo:TC -> TR,cooked:B.Pack<HC,TC>) -> B.Pack<HR,TR>:
13	  match cooked:
14	    case B.Pack{head,tail}: B.Pack{headUndo(head),tailUndo(tail)}
15	def constructed_tail(~Ctx:Type,~HR:Type,~HC:Type,~TR:Type,~TC:Type,~Error:Data,head:HC,headUndo:HC -> HR,tail:Staged<Ctx,TR,TC,Error>) -> Staged<Ctx,B.Pack<HR,TR>,B.Pack<HC,TC>,Error>:
16	  match tail:
17	    case Valid{ctx,cooked,undo,positions}: Valid{ctx,B.Pack{head,cooked},p => undo_pack(~HR,~HC,~TR,~TC,headUndo,undo,p),None{} <> positions}
18	    case Failed{ctx,raw,positions}: Failed{ctx,B.Pack{headUndo(head),raw},None{} <> positions}
19	def invalid_tail(~Ctx:Type,~HR:Type,~HC:Type,~TR:Type,~TC:Type,~Error:Data,head:HR,error:Error,tail:Staged<Ctx,TR,TC,Error>) -> Staged<Ctx,B.Pack<HR,TR>,B.Pack<HC,TC>,Error>:
20	  match tail:
21	    case Valid{ctx,cooked,undo,positions}: Failed{ctx,B.Pack{head,undo(cooked)},Some{error} <> positions}
22	    case Failed{ctx,raw,positions}: Failed{ctx,B.Pack{head,raw},Some{error} <> positions}
23	def constructed_head(~Ctx:Type,~HR:Type,~HC:Type,~TR:Type,~TC:Type,~Error:Data,~stageTail:Ctx -> TR -> Staged<Ctx,TR,TC,Error>,tail:TR,observed:Ctx & Construction<HR,HC,Error>) -> Staged<Ctx,B.Pack<HR,TR>,B.Pack<HC,TC>,Error>:
24	  match observed:
25	    case (ctx,Constructed{head,undo}): constructed_tail(~Ctx,~HR,~HC,~TR,~TC,~Error,head,undo,stageTail(ctx,tail))
26	    case (ctx,Invalid{head,error}): invalid_tail(~Ctx,~HR,~HC,~TR,~TC,~Error,head,error,stageTail(ctx,tail))
27	def stage(~Ctx:Type,~HR:Type,~HC:Type,~TR:Type,~TC:Type,~Error:Data,~constructHead:Ctx -> HR -> Ctx & Construction<HR,HC,Error>,~stageTail:Ctx -> TR -> Staged<Ctx,TR,TC,Error>,ctx:Ctx,raw:B.Pack<HR,TR>) -> Staged<Ctx,B.Pack<HR,TR>,B.Pack<HC,TC>,Error>:
28	  match raw:
29	    case B.Pack{head,tail}: constructed_head(~Ctx,~HR,~HC,~TR,~TC,~Error,~stageTail,tail,constructHead(ctx,head))
30	def terminal(~Ctx:Type,~Error:Data,ctx:Ctx,raw:Unit) -> Staged<Ctx,Unit,Unit,Error>:
31	  Valid{ctx,Unit{},u => u,[]}