Reading declarations from a file.

• §1. Keeping the syntax module happy
• §2. REPL variables
• §3. A sort of REPL

§1. Keeping the syntax module happy.We are going to need to use the sentence-breaking apparatus from the syntax module, which means that the following four nonterminals need to exist. But in fact they are really just placeholders — they are wired so that they can never match any text.

<dividing-sentence>
    ...

<structural-sentence>
    ...

<language-modifying-sentence>
    ...

<comma-divisible-sentence>
    ...

§2. REPL variables.

enum repl_var_CLASS
enum named_function_CLASS
enum named_unary_predicate_CLASS

DECLARE_CLASS(repl_var)
DECLARE_CLASS(named_function)
DECLARE_CLASS(named_unary_predicate)

typedef struct repl_var {
    struct wording name;
    struct pcalc_prop *val;
    CLASS_DEFINITION
} repl_var;

typedef struct named_function {
    struct wording name;
    struct binary_predicate *bp;
    int side;
    CLASS_DEFINITION
} named_function;

typedef struct named_unary_predicate {
    struct wording name;
    struct unary_predicate *up;
    CLASS_DEFINITION
} named_unary_predicate;

<new-repl-variable> internal
    repl_var *rv;
    LOOP_OVER(rv, repl_var)
        if (Wordings::match(rv->name, W)) {
            ==> { -, rv }; return TRUE;
        }
    rv = CREATE(repl_var);
    rv->val = NULL;
    rv->name = W;
    ==> { -, rv }; return TRUE;
}

<repl-variable> internal
    repl_var *rv;
    LOOP_OVER(rv, repl_var)
        if (Wordings::match(rv->name, W)) {
            ==> { -, rv }; return TRUE;
        }
    return FALSE;
}

<named-function> internal
    named_function *nf;
    LOOP_OVER(nf, named_function)
        if (Wordings::match(nf->name, W)) {
            ==> { -, nf }; return TRUE;
        }
    return FALSE;
}

<unary-name> internal
    named_unary_predicate *nup;
    LOOP_OVER(nup, named_unary_predicate)
        if (Wordings::match(nup->name, W)) {
            ==> { -, nup->up }; return TRUE;
        }
    return FALSE;
}

• The structure repl_var is accessed in 2/trs, 4/prp, 4/jsn, 5/mrk, 5/mv, 5/im, 7/ld, 8/ws, 8/ws2, 8/hs, 8/wcl, 9/pl, 9/cs, 10/ts, 10/pt, 10/wt, 11/rw, 11/cl, 3/tff, 1/sc, 2/art, 2/prn, 3/dmn, 5/smp and here.
• The structure named_function is accessed in 2/trs, 4/prp, 4/jsn, 5/mrk, 5/mv, 5/im, 7/ld, 8/ws, 8/ws2, 8/hs, 8/wcl, 9/pl, 9/cs, 10/ts, 10/pt, 10/wt, 11/rw, 11/cl, 3/tff, 1/sc, 2/art, 2/prn, 3/dmn, 4/trm, 4/tcp, 5/smp and here.
• The structure named_unary_predicate is accessed in 2/trs, 4/prp, 4/jsn, 5/mrk, 5/mv, 5/im, 7/ld, 8/ws, 8/ws2, 8/hs, 8/wcl, 9/pl, 9/cs, 10/ts, 10/pt, 10/wt, 11/rw, 11/cl, 3/tff, 1/sc, 2/art, 2/prn, 3/dmn, 5/smp and here.

§3. A sort of REPL.The following function reads a file whose name is in arg, feeds it into the lexer, builds a syntax tree of its sentences, and then walks through that tree, applying the Preform nonterminal <declaration-line> to each sentence. In effect, this is a read-evaluate-print loop.

parse_node_tree *syntax_tree = NULL;
text_stream *test_err = NULL;

void Declarations::load_from_file?Usage of Declarations::load_from_file:
Program Control - §2(text_stream *arg) {
    filename *F = Filenames::from_text(arg);
    feed_t FD = Feeds::begin();
    source_file *sf = TextFromFiles::feed_into_lexer(F, NULL_GENERAL_POINTER);
    wording W = Feeds::end(FD);
    if (sf == NULL) { PRINT("File has failed to open\n"); return; }
    syntax_tree = SyntaxTree::new();
    Sentences::break(syntax_tree, W);
    BinaryPredicateFamilies::first_stock();
    test_err = Str::new();
    SyntaxTree::traverse(syntax_tree, Declarations::parse);
}

void Declarations::parse(parse_node *p) {
    if (Node::get_type(p) == SENTENCE_NT) {
        wording W = Node::get_text(p);
        <declaration-line>(W);
    }
}

§4.

<declaration-line>
    new unary ### |
    new binary ### ( ### , ### ) |
    set <new-repl-variable> to <evaluation> |
    term <term> |
    constant underlying <term> |
    variable underlying <term> |
    variable unused in <evaluation> |
    variables in <evaluation> |
    <evaluation> |
    <test> |
    ...

<evaluation>
    ( <evaluation> ) |
    <evaluation> concatenate <evaluation> |
    <evaluation> conjoin <evaluation> |
    copy of <evaluation> |
    negation of <evaluation> |
    unnegation of <evaluation> |
    renumbering of <evaluation> |
    binding of <evaluation> |
    substitution of <term> = <term> in <evaluation> |
    insert <evaluation> at <cardinal-number> in <evaluation> |
    delete <cardinal-number> from <evaluation> |
    remove universal quantifier from <evaluation> |
    remove close domain from <evaluation> |
    <repl-variable> |
    <proposition>

<test>
    <evaluation> is syntactically valid |
    <evaluation> is well-formed  |
    <evaluation> is complex |
    <evaluation> contains relation |
    <evaluation> contains quantifier |
    <evaluation> is a group

<proposition>
    << <atoms> >> |
    << <quantification> >> |
    << >>

<atoms>
    <quantification> \: <atoms> |
    <quantification> in< <atoms> in> \: <atoms> |
    not< <atoms> not> |
    <atomic-proposition> \^ <atoms> |
    <atomic-proposition>

<atomic-proposition>
    <unary-name> ( <term> ) |
    ( <term> == <term> ) |
    <relation-name> ( <term> , <term> ) |
    kind = <k-kind> ( <term> ) |
    not< |
    not> |
    in< |
    in>

<term>
    <pcvar> |
    <cardinal-number> |
    <named-function> ( <term> ) |
    first cited in <evaluation>

<quantification>
    <quantifier> <pcvar>

<quantifier>
    ForAll |
    NotAll |
    Exists |
    DoesNotExist |
    AllBut <cardinal-number> |
    NotAllBut <cardinal-number> |
    Proportion>=80% |
    Proportion<20% |
    Proportion>50% |
    Proportion<=50% |
    Card>= <cardinal-number> |
    Card<= <cardinal-number> |
    Card= <cardinal-number> |
    Card< <cardinal-number> |
    Card> <cardinal-number> |
    Card~= <cardinal-number>

<pcvar>
    x |
    y |
    z

§4.1. Substitution4.1 =

    pcalc_term *V = RP[1];
    pcalc_term *T = RP[2];
    pcalc_prop *P = RP[3];
    int bogus = 0;
    ==> { -, Binding::substitute_term(P, V->variable, *T, FALSE, &bogus, &bogus) }

• This code is used in §4.

§4.2. Insert4.2 =

    pcalc_prop *P = RP[3];
    pcalc_prop *pos = NULL;
    for (int i=0; i<R[2]; i++) pos = (pos == NULL)?P:(pos->next);
    ==> { -, Propositions::insert_atom(P, pos, RP[1]) }

• This code is used in §4.

§4.3. Delete4.3 =

    pcalc_prop *P = RP[2];
    pcalc_prop *pos = NULL;
    for (int i=0; i<R[1]; i++) pos = (pos == NULL)?P:(pos->next);
    ==> { -, Propositions::delete_atom(P, pos) }

• This code is used in §4.

§4.4. Make domain4.4 =

    ==> { -, Propositions::quantify_using(RP[1], RP[2], RP[3]) }

• This code is used in §4.

§4.5. Create new unary4.5 =

    Declarations::new_unary(GET_RW(<declaration-line>, 1), K_number);
    PRINT("'%<W': ok\n", W);

• This code is used in §4.

§4.6. Create new binary4.6 =

    Declarations::new(GET_RW(<declaration-line>, 1),
        K_number, GET_RW(<declaration-line>, 2), K_number, GET_RW(<declaration-line>, 3));
    PRINT("'%<W': ok\n", W);

• This code is used in §4.

§4.7. Set REPL var4.7 =

    pcalc_prop *P = RP[2];
    repl_var *rv = RP[1];
    rv->val = P;
    PRINT("'%<W': %W set to ", W, rv->name);
    Propositions::write(STDOUT, P);
    PRINT("\n");

• This code is used in §4.

§4.8. Show term4.8 =

    pcalc_term *T = RP[1];
    PRINT("'%<W': ", W);
    Terms::write(STDOUT, T);
    PRINT("\n");

• This code is used in §4.

§4.9. Show const underlying4.9 =

    pcalc_term *T = RP[1];
    PRINT("'%<W': ", W);
    parse_node *val = Terms::constant_underlying(T);
    if (val == NULL) PRINT("--"); else PRINT("'%W'", Node::get_text(val));
    PRINT("\n");

• This code is used in §4.

§4.10. Show var underlying4.10 =

    pcalc_term *T = RP[1];
    PRINT("'%<W': ", W);
    int v = Terms::variable_underlying(T);
    if (v < 0) PRINT("--"); else PRINT("%c", pcalc_vars[v]);
    PRINT("\n");

• This code is used in §4.

§4.11. Show var unused4.11 =

    pcalc_prop *P = RP[1];
    PRINT("'%<W': ", W);
    int v = Binding::find_unused(P);
    if (v < 0) PRINT("--"); else PRINT("%c", pcalc_vars[v]);
    PRINT("\n");

• This code is used in §4.

§4.12. Show result4.12 =

    pcalc_prop *P = RP[1];
    PRINT("'%<W': ", W);
    Propositions::write(STDOUT, P);
    PRINT("\n");

• This code is used in §4.

§4.13. Show result of test4.13 =

    PRINT("'%<W': ", W);
    if (R[1]) PRINT("true"); else {
        PRINT("false");
        if (Str::len(test_err) > 0) PRINT(" - %S", test_err);
    }
    Str::clear(test_err);
    PRINT("\n");

• This code is used in §4.

§4.14. Show variable status4.14 =

    int var_states[26];
    TEMPORARY_TEXT(err)
    int happy = Binding::determine_status(RP[1], var_states, err);
    PRINT("'%<W':", W);
    if (happy) {
        PRINT(" valid:");
        for (int v=0; v<26; v++) {
            if (var_states[v] == FREE_VST) PRINT(" %c free", pcalc_vars[v]);
            if (var_states[v] == BOUND_VST) PRINT(" %c bound", pcalc_vars[v]);
        }
    } else {
        PRINT(" invalid: %S", err);
    }
    DISCARD_TEXT(err)
    PRINT("\n");

• This code is used in §4.

§4.15. Fail with error4.15 =

    PRINT("Declaration not understood: '%W'\n", W);
    ==> { fail }

• This code is used in §4.

§5.

bp_family *test_bp_family = NULL;
up_family *test_up_family = NULL;

void Declarations::new_unary?Usage of Declarations::new_unary:
§4.5(wording W, kind *k0) {
    if (test_up_family == NULL) {
        test_up_family = UnaryPredicateFamilies::new();
        METHOD_ADD(test_up_family, LOG_UPF_MTID, Declarations::log_unary);
    }
    named_unary_predicate *nup = CREATE(named_unary_predicate);
    nup->up = UnaryPredicates::new(test_up_family);
    nup->up->assert_kind = k0;
    nup->up->calling_name = W;
    nup->name = W;
}

void Declarations::new?Usage of Declarations::new:
§4.6(wording W, kind *k0, wording f0, kind *k1, wording f1) {
    if (test_bp_family == NULL)
        test_bp_family = BinaryPredicateFamilies::new();
    bp_term_details t0 =
        BPTerms::new(TERM_DOMAIN_FROM_KIND_FUNCTION(k0));
    bp_term_details t1 =
        BPTerms::new(TERM_DOMAIN_FROM_KIND_FUNCTION(k1));
    text_stream *S = Str::new();
    WRITE_TO(S, "%W", W);
    binary_predicate *bp =
        BinaryPredicates::make_pair(test_bp_family, t0, t1, S, NULL, NULL,
            Calculus::Schemas::new("%S(*1, *2)", S),
            WordAssemblages::from_wording(W));
    TEMPORARY_TEXT(f0n)
    TEMPORARY_TEXT(f1n)
    WRITE_TO(f0n, "%W", f0);
    WRITE_TO(f1n, "%W", f1);
    if (Str::ne(f0n, I"none")) {
        named_function *nf = CREATE(named_function);
        nf->bp = bp;
        nf->name = f0;
        nf->side = 1;
        BPTerms::set_function(&(bp->term_details[0]),
            Calculus::Schemas::new("%S(*1)", f0n));
    }
    if (Str::ne(f1n, I"none")) {
        named_function *nf = CREATE(named_function);
        nf->bp = bp;
        nf->name = f1;
        nf->side = 0;
        BPTerms::set_function(&(bp->term_details[1]),
            Calculus::Schemas::new("%S(*1)", f1n));
    }
    DISCARD_TEXT(f0n)
    DISCARD_TEXT(f1n)
}

int stashed = 0;
pcalc_term stashed_terms[1000];

pcalc_term *Declarations::stash?Usage of Declarations::stash:
§4(pcalc_term t) {
    if (stashed == 1000) internal_error("too many terms in test case");
    stashed_terms[stashed] = t;
    return &(stashed_terms[stashed++]);
}

parse_node *Declarations::number_to_value?Usage of Declarations::number_to_value:
§4(wording W, int n) {
    return Diagrams::new_UNPARSED_NOUN(W);
}

void Declarations::log_unary(up_family *self, OUTPUT_STREAM, unary_predicate *up) {
    WRITE("%W", up->calling_name);
}