Partial

614⟨dom: Partial 614⟩≡   (613)
Partial(S:Type): with {
        ⟨exports: Partial 615⟩
} == add {
        Rep == Record(failed?: Boolean, val: S);
        import from Rep, Boolean;
        ⟨implementation: Partial 616⟩
}

Defines:
Partial, used in chunks 428b and 617.

Exports of Partial

: bracket: S -> %
: failed: %
: failed?: % -> Boolean
: retract: % -> S
: if S has PrimitiveType then PrimitiveType;
: if S has OutputType then OutputType;
: if S has SetCategory then SetCategory;

615⟨exports: Partial 615⟩≡ (614)
bracket: S -> %;
failed: %;
failed?: % -> Boolean;
retract: % -> S;
if S has PrimitiveType then PrimitiveType;
if S has OutputType then OutputType;
if S has SetCategory then SetCategory;

Uses OutputType 570.

616⟨implementation: Partial 616⟩≡   (614)
failed: %               == per [true, true pretend S];
failed?(x: %): Boolean  == (rep x).failed?;
[x: S]: %               == per [false, x];

retract(x:%): S         == {
        import from Boolean;
        assert(~failed? x);
        rep(x).val;
}

if S has PrimitiveType or S has SetCategory then {
        (x:%) = (y:%):Boolean == {
                import from S;
                fy? := failed? y;
                failed? x => fy?;
                ~fy? and retract x = retract y;
        }
}

if S has OutputType then {
        (tw: TextWriter) << (x: %): TextWriter == {
                import from String;
                failed? x => tw << "failed";
                tw << "[" << retract x << "]";
        }
}

Uses OutputType 570 and String 65.

23.1 Partial