vars kpl_original_output_file;

if vedlmr_print_in_file /= 'checker output.p' then
    vedlmr_print_in_file -> kpl_original_output_file;
    'checker output.p' -> vedlmr_print_in_file;
endif;

;;; compile('~kpl/Project/utils.p');

define islogsymbol(item) -> bool;
    lvars item, bool;
    item == "top" or item == "bottom"
    or item == "=" or item == "~"
    or item == "/\" or item == "\/"
    or item == "->" or item == "<->"
    or item == "all" or item == "exists"
    -> bool;
enddefine;

define ispred(input, lang) -> arity;
    lvars input, lang, arity=false, pair;
    for pair in lang(1) do
        if front(pair) == input then
            back(pair) -> arity;
            quitloop;
        endif;
    endfor;
enddefine;

define isfunc(input, lang) -> arity;
    lvars input, lang, arity=false, pair;
    for pair in lang(2) do
        if front(pair) == input then
            back(pair) -> arity;
            quitloop;
        endif;
    endfor;
enddefine;

define isvar(input, lang) -> bool;
    lvars input, lang, bool=false, letter;

    if isword(input) then
        lvars tailstring=substring(2, datalength(input)-1, input);

        if member(substring(1, 1, input), ['u' 'v' 'w' 'x' 'y' 'z'])
        and (strnumber(tailstring) or tailstring=nullstring)
        and not(ispred(input, lang))
        and not(isfunc(input, lang))
        then
            true -> bool;
        endif;
    endif;
enddefine;

define remove_commas(input) -> output;
    lvars input, output=[], item;
    for item in input do
        if item /== "," then
            [^^output ^item] -> output;
        endif;
    endfor;
enddefine;

define isnatural(num) -> bool;
    lvars num, bool;
    isinteger(num) and num >= 0 -> bool;
enddefine;

define nested_list_member(item, list) -> bool;
    lvars item, list, bool=false, element;
    for element in list do
        if element=item then
            true -> bool;
            quitloop;
        else
            islist(element) and nested_list_member(item, element) -> bool;
            quitif(bool);
        endif;
    endfor;
enddefine;

define remove_dups(list) -> new_list;
    lvars list, new_list=[], item;
    for item in list do
        if not(member(item,new_list)) then
            item :: new_list -> new_list;
        endif;
    endfor;
    rev(new_list) -> new_list;
enddefine;

define tnpr(output);
    lvars output;
    tabs(1);
    npr(output);
enddefine;

define ttnpr(output);
    lvars output;
    tabs(2);
    npr(output);
enddefine;

define tpr(output);
    lvars output;
    tabs(1);
    pr(output);
enddefine;

define ttpr(output);
    lvars output;
    tabs(2);
    pr(output);
enddefine;

define line_break_spr(list, tab_indent, line_so_far);
    lvars list, tab_indent, line_so_far, count, len, print_str,
        line_new_str='', line_str, include_space=true;

    for count to tab_indent do
        line_new_str >< '    ' -> line_new_str;
    endfor;

    if line_so_far then
        line_so_far -> line_str;
        while datalength(line_str) > vedwlinewidth - 10 do
            npr(substring(1,vedwlinewidth-10,line_str));
            substring(vedwlinewidth-9,datalength(line_str)-vedwlinewidth+10,line_str)
                -> line_str;
        endwhile;
        false -> include_space;

    else
        line_new_str -> line_str;
    endif;

    for count to (listlength(list) ->> len) do
        list(count) -> print_str;
        if count /== len then
            print_str >< ',' -> print_str;
        endif;
        if line_str = line_new_str or line_str = nullstring then
            line_str >< print_str -> line_str;

            while datalength(line_str) > vedwlinewidth - 10 do
                npr(substring(1,vedwlinewidth-10,line_str));
                line_new_str ><
                substring(vedwlinewidth-9,datalength(line_str)-vedwlinewidth+10,line_str)
                    -> line_str;
            endwhile;

        elseif datalength(line_str) + datalength(print_str) > vedwlinewidth - 11 then
            npr(line_str);
            line_new_str -> line_str;
            count - 1 -> count;
        else
            line_str;
            if include_space then
                >< space;
            else
                true -> include_space;
            endif;
            >< print_str -> line_str;
        endif;
    endfor;

    pr(line_str);
enddefine;

define tuple_generator(list, n) -> n_tuples;
    lvars list, n, n_tuples, item, tuple, n_1_tuples;
    if n==0 then
        [[]] -> n_tuples;
    else
        [] -> n_tuples;
        tuple_generator(list, n-1) -> n_1_tuples;
        for item in list do
            for tuple in n_1_tuples do
                [^^n_tuples [^item ^^tuple]] -> n_tuples;
            endfor;
        endfor;
    endif;
enddefine;

define convert_num(item) -> new_item;
    lvars item, new_item;
    if isnumber(item) then
        consword(item >< nullstring);
    else
        item;
    endif;
        -> new_item;
enddefine;

define convert_nums(list) -> new_list;
    lvars list, new_list, item;

    [% for item in list do
            convert_num(item);
        endfor; %] -> new_list;

enddefine;

define contains_symbol(symbols, str) -> (pos,symbol);
    lvars symbols, list, pos=false, symbol=false, item;
    ;;;Note prioritised : the earlier the symbol appears in symbols
    ;;;  the higher its priority.
    for item in symbols do
        if issubstring(item, str) ->> pos then
            item -> symbol;
            quitloop;
        endif;
    endfor;
enddefine;

define separate_symbols(str, symbols) -> list;
    lvars str, symbols, list, word=false, pos, start_str,
        symbol, symbol_len;
    [% if (isword(str) ->> word) or isstring(str) then
            if contains_symbol(symbols,str) -> symbol ->> pos then
                substring(1,pos-1,str);
                if word then
                    consword();
                endif;
                explode(separate_symbols(symbols));

                symbol;

                substring(pos+(datalength(symbol) ->> symbol_len),
                    datalength(str)-pos+1-symbol_len, str);
                if word then
                    consword();
                endif;
                explode(separate_symbols(symbols));

            elseif str/='' and str/==consword('') then
                str;
            endif;

        else
            str;
        endif; %] -> list;
enddefine;

define quick_sort(list, pred) -> sorted_list;
    lvars list, pred, sorted_list, item, list1=nil, list2=nil,
        head;

    if listlength(list) < 2 then
        list -> sorted_list;
    else
        hd(list) -> item;
        tl(list) -> list;
        until null(list) do
            if pred(hd(list) ->> head, item) then
                head :: list2 -> list2;
            else
                head :: list1 -> list1;
            endif;
            tl(list) -> list;
        enduntil;

        quick_sort(list1,pred) <> [^item] <> quick_sort(list2,pred) -> sorted_list;
    endif;
enddefine;

define prioritised_list(lang) -> list;
    lvars lang, list, item;
    [%for item in lang(1) do
            front(item);
        endfor;
        for item in lang(2) do
            front(item);
        endfor;
        "("; ")"; ","; "top"; "bottom";
        "="; "~"; "/\"; "\/"; "->";
        "<->"; "all"; "exists"; %];
    quick_sort(isstartstring) -> list;
enddefine;

define vbles_in_term(term) -> vbles;
    lvars term, vbles, arg;
    if islist(term) then
        remove_dups(
            [% for arg in tl(term) do
                    explode(vbles_in_term(arg));
                endfor; %]) -> vbles;
    else
        [^term] -> vbles;
    endif;
enddefine;

define frees_in_formula(formula, lang) -> frees;
    lvars formula, lang, frees=nil, arg, connective;

    if islist(formula) then
        hd(formula) -> connective;

        if ispred(connective,lang) or connective == "=" then
            remove_dups(
                [% for arg in tl(formula) do
                        explode(vbles_in_term(arg));
                    endfor; %]) -> frees;

        elseif connective=="~" then
            frees_in_formula(formula(2),lang) -> frees;

        elseif connective=="/\" or connective=="\/" or connective=="->"
        or connective=="<->" then
            remove_dups(
                [% for arg in tl(formula) do
                        explode(frees_in_formula(arg,lang));
                    endfor; %]) -> frees;

        elseif connective=="all" or connective=="exists" then
            delete(formula(2),
                frees_in_formula(formula(3),lang),
                valof("==")) -> frees;

        endif;

    endif;

enddefine;

define difference(list1, list2) -> list_diff;
    lvars list1, list2, list_diff, item;
    [%for item in list1 do
        if not(member(item,list2)) then
            item;
        endif;
    endfor; %] -> list_diff;
enddefine;

define find_lang_item(item_name, items) -> item_found;
    lvars item_name, items, item_found=false, item;

    for item in items do
        if front(item) == item_name then
            item -> item_found;
        endif;
    endfor;

enddefine;

define funcs_in_term(all_funcs, term) -> funcs;
    lvars all_funcs, term, funcs=nil, item;

    if islist(term) then
        remove_dups([% find_lang_item(hd(term), all_funcs);
            for item in tl(term) do
                explode(funcs_in_term(all_funcs, item));
            endfor; %]) -> funcs;
    endif;

enddefine;

define lang_union(lang1, lang2) -> new_lang;
    lvars lang1, lang2, new_lang;

    [% remove_dups([^^(lang1(1)) ^^(lang2(1))]);
        remove_dups([^^(lang1(2)) ^^(lang2(2))]);
    %] -> new_lang;

enddefine;

define lang_used_in_formula(lang, formula) -> sub_lang;
    lvars lang, formula, sub_lang, connective, term
        preds, funcs;

    if islist(formula) then
        hd(formula) -> connective;
        lang(1) -> preds;
        lang(2) -> funcs;

        if ispred(connective, lang) then
            [[% find_lang_item(connective, preds) %]
                %remove_dups([%for term in tl(formula) do
                        explode(funcs_in_term(funcs, term));
                    endfor; %]); %
            ] -> sub_lang;

        elseif connective == "=" then
            [^nil
                %remove_dups([%explode(funcs_in_term(funcs, formula(2)));
                    explode(funcs_in_term(funcs, formula(3))); %]); %
            ] -> sub_lang;

        elseif connective == "~" then
            lang_used_in_formula(lang, formula(2)) -> sub_lang;

        elseif connective == "/\" or connective == "\/"
            or connective == "->" or connective == "<->" then

            lang_union(lang_used_in_formula(lang, formula(2)),
                lang_used_in_formula(lang, formula(3))) -> sub_lang;

        elseif connective == "all" or connective == "exists" then
            lang_used_in_formula(lang, formula(3)) -> sub_lang;

        endif;
    else
        [[] []] -> sub_lang;
    endif;

enddefine;

define lang_difference(lang1, lang2) -> new_lang;
    lvars lang1, lang2, new_lang, preds1=lang1(1), preds2=lang2(1),
        funcs1=lang1(2), funcs2=lang2(2), pred, func;

    [[%for pred in preds1 do
                if not(member(pred, preds2)) then
                    pred;
                endif;
            endfor; %]
        [%for func in funcs1 do
                if not(member(func, funcs2)) then
                    func;
                endif;
            endfor; %]
    ] -> new_lang;

enddefine;


;;; compile('~kpl/Project/parser.p');

define parse_term(input, lang, vbles) -> term;
    lvars input, lang, vbles, term;
    lvars count, open_bracs=0, first_brac_pos, brac_contents, unbrac_input=[],
        item, argument, inner_count, arity;

    if isword(input) then

        if member(input, vbles) then

            input -> term;

        elseif isfunc(input, lang) == 0 then

            [^input] -> term;

        else

            'Illformed term : variable or constant expected' -> term;

        endif;

    elseif length(input) > 0 then

        for count to length(input) do

            if islist(unbrac_input) then

                if input(count)=="(" then

                    open_bracs+1->open_bracs;
                    if open_bracs==1 then
                        count -> first_brac_pos;
                        [] -> brac_contents;
                    else
                        [^^brac_contents ^(input(count))] -> brac_contents;
                    endif;

                elseif input(count)==")" then

                    open_bracs-1->open_bracs;
                    if open_bracs<0 then
                        'Illformed term : too many closing brackets' -> unbrac_input;
                        quitloop;
                    elseif open_bracs==0 then

                        if first_brac_pos>1 and
                            isfunc(input(first_brac_pos-1),lang) then

                            [^^unbrac_input [^(input(first_brac_pos-1))
                                    ^^brac_contents]] -> unbrac_input;

                        else

                            'Illformed term : brackets found with no preceding '
                            <> 'function symbol' -> unbrac_input;

                        endif;

                    else
                        [^^brac_contents ^(input(count))] -> brac_contents;
                    endif;

                elseif open_bracs==0 then

                    if not(isfunc(input(count),lang)) or
                        (length(input)==count or input(count+1)/=="(") then

                        [^^unbrac_input ^(input(count))] -> unbrac_input;

                    endif;

                elseif open_bracs>0 then

                    [^^brac_contents ^(input(count))] -> brac_contents;

                endif;

            endif;

        endfor;

        if open_bracs>0 then

            'Illformed term : not enough closing brackets' -> unbrac_input;

        endif;

        if isstring(unbrac_input) then

            unbrac_input -> term;

        elseif unbrac_input==[] then

            'Illformed term : empty term' -> term;

        else

            isfunc(hd(unbrac_input),lang) -> arity;

            if arity == length(unbrac_input)-1 then

                [^(hd(unbrac_input))] -> term;

                for item in tl(unbrac_input) do

                    parse_term(item, lang, vbles) -> argument;
                    if isstring(argument) then
                        argument->term;
                        quitloop;
                    else
                        [^^term ^argument] -> term;
                    endif;

                endfor;

            elseif isnumber(arity) then

                'Illformed term : incorrect number of arguments in function '
                >< hd(unbrac_input) -> term;

            elseif length(unbrac_input)==1 then
                parse_term(hd(unbrac_input),lang,vbles)->term;

            else

                'Illformed term' -> term;

            endif;

        endif;

    else

        'Illformed term : empty term' -> term;

    endif;

enddefine;

define parse_formula(input, lang, vbles) -> formula;
    lvars input, lang, vbles, formula;
    lvars count, open_bracs=0, first_brac_pos, inner_count, brac_contents,
        unbrac_input=[], item, argument, left_form, right_form, left_term,
        right_term, arity;
    lvars num_implies=0, num_iff=0, num_and=0, num_or=0;

    vars left_of, right_of, symbol;

    if not(isword(input)) and not(islist(input)) then

        'Illformed formula' -> formula;

    elseif isword(input) then

        if input=="top" or input=="bottom" then

            input->formula;

        else

            'Illformed formula : top or bottom expected' -> formula;

        endif;

    elseif length(input) > 0 then

        for count to length(input) do

            if islist(unbrac_input) then

                if input(count)=="(" then

                    open_bracs+1->open_bracs;
                    if open_bracs==1 then
                        count -> first_brac_pos;
                        [] -> brac_contents;
                    else
                        [^^brac_contents ^(input(count))] -> brac_contents;
                    endif;

                elseif input(count)==")" then

                    open_bracs-1->open_bracs;
                    if open_bracs<0 then
                        'Illformed formula : too many closing brackets'
                            -> unbrac_input;
                        quitloop;

                    elseif open_bracs==0 then

                        if first_brac_pos>1 and
                            ( ispred(input(first_brac_pos-1),lang) or
                                isfunc(input(first_brac_pos-1),lang) ) then

                            [^^unbrac_input
                                [^(input(first_brac_pos-1)) ^^brac_contents]]
                                -> unbrac_input;

                        else

                            [^^unbrac_input ^brac_contents] -> unbrac_input;

                        endif;

                    else
                        [^^brac_contents ^(input(count))] -> brac_contents;
                    endif;

                elseif open_bracs==0 then

                    if not(ispred(input(count),lang) or isfunc(input(count),lang))
                    or (length(input)==count or input(count+1)/=="(") then

                        [^^unbrac_input ^(input(count))] -> unbrac_input;

                    endif;

                elseif open_bracs>0 then

                    [^^brac_contents ^(input(count))] -> brac_contents;

                endif;

            endif;

        endfor;

        if open_bracs>0 then

            'Illformed formula : not enough closing brackets' -> unbrac_input;

        endif;

        if isstring(unbrac_input) then

            unbrac_input -> formula;

        elseif unbrac_input==[] then

            'Illformed formula : empty formula' -> formula;

        else

            for count to length(unbrac_input) do

                if unbrac_input(count) == "->" then
                    num_implies+1 -> num_implies;
                elseif unbrac_input(count) == "<->" then
                    num_iff+1 -> num_iff;
                elseif unbrac_input(count) == "/\" then
                    num_and+1 -> num_and;
                elseif unbrac_input(count) == "\/" then
                    num_or+1 -> num_or;
                endif;

            endfor;

            if num_implies>=2 or (num_implies>=1 and num_iff>=1) then
                'Ambiguous formula : too many implications' -> formula;
            elseif num_and>=1 and num_or>=1 then
                'Ambiguous formula : mixed /\\\'s and \\/\'s' -> formula;
            else
                if unbrac_input matches [??left_of
                        ?symbol:%procedure(l); l=="->" or l=="<->"; endprocedure%
                        ??right_of] or

                    unbrac_input matches [??left_of
                        ?symbol:%procedure(l); l=="/\" or l=="\/"; endprocedure%
                        ??right_of] then

                    parse_formula(left_of,lang,vbles)->left_form;
                    parse_formula(right_of,lang,vbles)->right_form;
                    if isstring(left_form) then
                        left_form->formula;
                    elseif isstring(right_form) then
                        right_form->formula;
                    else
                        [^symbol ^left_form ^right_form] -> formula;
                    endif;

                elseif hd(unbrac_input)=="~" then
                    parse_formula(tl(unbrac_input),lang,vbles)->right_form;
                    if isstring(right_form) then
                        right_form->formula;
                    else
                        [~ ^right_form] -> formula;
                    endif;

                elseif hd(unbrac_input)=="all" or hd(unbrac_input)=="exists" then
                    if not(null(tl(unbrac_input))) and
                        member(hd(tl(unbrac_input)),vbles) then

                        parse_formula(tl(tl(unbrac_input)),lang,vbles)->right_form;
                        if isstring(right_form) then
                            right_form->formula;
                        else
                            [^(hd(unbrac_input)) ^(hd(tl(unbrac_input)))
                                ^right_form] -> formula;
                        endif;
                    else
                        'Illformed formula : quantifier present without a variable'
                            -> formula;
                    endif;

                elseif (ispred(hd(unbrac_input),lang) ->> arity) ==
                    length(unbrac_input)-1 then

                    [^(hd(unbrac_input))] -> formula;
                    for item in tl(unbrac_input) do
                        parse_term(item,lang,vbles) -> argument;
                        if isstring(argument) then
                            argument->formula;
                            quitloop;
                        else
                            [^^formula ^argument] -> formula;
                        endif;
                    endfor;

                elseif isnumber(arity) then

                    'Illformed formula : incorrect number of arguments in predicate '
                    >< hd(unbrac_input) -> formula;

                elseif length(unbrac_input)==3 and unbrac_input(2)=="=" then
                    parse_term(unbrac_input(1),lang,vbles)->left_term;
                    parse_term(unbrac_input(3),lang,vbles)->right_term;
                    if isstring(left_term) then
                        left_term->formula;
                    elseif isstring(right_term) then
                        right_term->formula;
                    else
                        [= ^left_term ^right_term] -> formula;
                    endif;

                elseif length(unbrac_input)==1 then
                    parse_formula(hd(unbrac_input),lang,vbles)->formula;

                else
                    'Illformed formula' -> formula;

                endif;

            endif;

        endif;

    else

        'Illformed formula : empty formula' -> formula;

    endif;

enddefine;

;;; compile('~kpl/Project/checker.p');

define assign(lang, vbles, interp, assignment, term) -> indiv;
    lvars lang, vbles, interp, assignment, term, indiv=false, arity, item;
    if member(term, vbles) then
        assignment(term) -> indiv;
    elseif islist(term) then
        isfunc(hd(term), lang) -> arity;
        if arity then
            if arity==0 then
                interp("funcs")(hd(term)) -> indiv;
            elseif arity==1 then
                interp("funcs")(hd(term))
                (assign(lang,vbles,interp,assignment,term(2))) -> indiv;

            elseif arity>1 then
                interp("funcs")(hd(term))
                ([%
                        for item in tl(term) do
                            assign(lang, vbles, interp, assignment, item);
                        endfor;
                    %]) -> indiv;
            endif;
        endif;
    endif;
enddefine;

define satisfies(lang, vbles, interp, assignment, formula) -> bool;
    lvars lang, vbles, interp, assignment, formula, bool, arity, item,
        temp_assignment;
    vars connective, first, second;

    if isword(formula) then
        if formula == "top" then
            true -> bool;
        elseif formula == "bottom" then
            false -> bool;
        endif;

    elseif length(formula) > 0 then

        ispred(hd(formula), lang) -> arity;
        if arity then
            if arity == 0 then
                interp("preds")(hd(formula)) -> bool;
            elseif arity == 1 then
                if member(assign(lang, vbles, interp, assignment, formula(2)),
                        interp("preds")(hd(formula))) then
                    true -> bool;
                else
                    false -> bool;
                endif;
            elseif arity > 1 then
                if member([%
                            for item in tl(formula) do
                                assign(lang, vbles, interp, assignment, item);
                            endfor;
                        %],
                        interp("preds")(hd(formula))) then
                    true -> bool;
                else
                    false -> bool;
                endif;
            endif;

        elseif formula matches [?connective ?first ?second] then
            if connective == "=" then
                if assign(lang, vbles, interp, assignment, first) ==
                    assign(lang, vbles, interp, assignment, second) then
                    true -> bool;
                else
                    false -> bool;
                endif;

            elseif connective == "/\" then
                if satisfies(lang, vbles, interp, assignment, first) and
                    satisfies(lang, vbles, interp, assignment, second) then
                    true -> bool;
                else
                    false -> bool;
                endif;

            elseif connective == "\/" then
                if satisfies(lang, vbles, interp, assignment, first) or
                    satisfies(lang, vbles, interp, assignment, second) then
                    true -> bool;
                else
                    false -> bool;
                endif;

            elseif connective == "->" then
                if not(satisfies(lang, vbles, interp, assignment, first)) or
                    satisfies(lang, vbles, interp, assignment, second) then
                    true -> bool;
                else
                    false -> bool;
                endif;

            elseif connective == "<->" then
                if (satisfies(lang, vbles, interp, assignment, first) and
                        satisfies(lang, vbles, interp, assignment, second))
                or
                    (not(satisfies(lang, vbles, interp, assignment, first)) and
                        not(satisfies(lang, vbles, interp, assignment, second)))
                then
                    true -> bool;
                else
                    false -> bool;
                endif;

            elseif connective == "all" then
                true -> bool;
                copy(assignment) -> temp_assignment;
                for item in interp("univ") do
                    item -> temp_assignment(first);
                    if not(satisfies(lang, vbles, interp, temp_assignment, second)) then
                        false -> bool;
                        quitloop;
                    endif;
                endfor;

            elseif connective == "exists" then
                false -> bool;
                copy(assignment) -> temp_assignment;
                for item in interp("univ") do
                    item -> temp_assignment(first);
                    if satisfies(lang, vbles, interp, temp_assignment, second) then
                        true -> bool;
                        quitloop;
                    endif;
                endfor;

            endif;

        elseif formula matches [~ ?first] then
            if satisfies(lang, vbles, interp, assignment, first) then
                false -> bool;
            else
                true -> bool;
            endif;

        endif;
    endif;
enddefine;

define sat_all_assignments(lang, vbles, unassigned_vbles, interp, univ, assignment, formula) -> bool;
    lvars lang, vbles, unassigned_vbles, interp, univ, assignment,
        formula, bool=true, indiv;
    if null(unassigned_vbles) then
        satisfies(lang, vbles, interp, assignment, formula) -> bool;
    else
        for indiv in univ do
            indiv -> assignment(hd(unassigned_vbles));
            if not(sat_all_assignments(lang, vbles, tl(unassigned_vbles), interp, univ, assignment, formula)) then
                false -> bool;
                quitloop;
            endif;
        endfor;
    endif;
enddefine;


;;; compile('~kpl/Project/inverse_parser.p');

define inverse_parse_term(term) -> str;
    lvars term, str, len, count;
    if isword(term) then
        word_string(term) -> str;
    elseif (listlength(term) ->> len) == 1 then
        word_string(hd(term)) -> str;
    else
        word_string(hd(term)) <> '(' -> str;
        for count from 1 to len - 2 do
            str <> inverse_parse_term(tl(term)(count)) <> ',' -> str;
        endfor;
        str <> inverse_parse_term(tl(term)(len - 1)) <> ')' -> str;
    endif;
enddefine;

define is_pred_form(formula) -> bool;
    lvars formula, bool;
    if (islist(formula) ->> bool) then
        hd(formula) /== "all" and
        hd(formula) /== "exists" and
        hd(formula) /== "->" and
        hd(formula) /== "<->" and
        hd(formula) /== "/\" and
        hd(formula) /== "\/" and
        hd(formula) /== "~" and
        hd(formula) /== "=" -> bool;
    endif;
enddefine;

define inverse_parse_formula(formula) -> str;
    lvars formula, str, len, count, sub_strs;
    if isword(formula) then
        word_string(formula) -> str;

    elseif is_pred_form(formula) then
        word_string(hd(formula)) -> str;
        if (length(formula) ->> len) > 1 then
            str <> '(' -> str;
            for count from 1 to len - 2 do
                str <> inverse_parse_term(tl(formula)(count)) <> ',' -> str;
            endfor;
            str <> inverse_parse_term(tl(formula)(len - 1)) <> ')' -> str;
        endif;

    elseif hd(formula) == "=" then
        inverse_parse_term(formula(2)) <> ' = '
        <> inverse_parse_term(formula(3)) -> str;

    elseif hd(formula) == "~" then
        inverse_parse_formula(formula(2)) -> str;
        if islist(formula(2)) then
            if hd(formula(2)) == "/\" or hd(formula(2)) == "\/" or
                hd(formula(2)) == "->" or hd(formula(2)) == "<->" or
                hd(formula(2)) == "=" then
                '(' <> str <> ')' -> str;
            endif;
        endif;
        '~' <> str -> str;

    elseif hd(formula) == "/\" or hd(formula) == "\/" then
        [^(inverse_parse_formula(formula(2)))
            ^(inverse_parse_formula(formula(3)))] -> sub_strs;
        [%
            for count from 2 to 3 do
                if islist(formula(count)) then
                    if hd(formula(count)) == "<->" or hd(formula(count)) == "->" or
                        ((hd(formula(count))=="/\" or hd(formula(count))=="\/") and
                            hd(formula(count))/==hd(formula)) then

                        '(' <> sub_strs(count-1) <> ')';
                    else
                        sub_strs(count-1);
                    endif;
                else
                    sub_strs(count-1);
                endif;
            endfor;
        %] -> sub_strs;
        sub_strs(1) <> ' ' <> word_string(hd(formula)) <> ' ' <> sub_strs(2) -> str;

    elseif hd(formula) == "<->" or hd(formula) == "->" then
        [^(inverse_parse_formula(formula(2)))
            ^(inverse_parse_formula(formula(3)))] -> sub_strs;
        [%
            for count from 2 to 3 do
                if islist(formula(count)) then
                    if hd(formula(count)) == "->" or
                        (hd(formula(count)) == "<->" and
                            hd(formula) == "->") then

                        '(' <> sub_strs(count-1) <> ')';
                    else
                        sub_strs(count-1);
                    endif;
                else
                    sub_strs(count-1);
                endif;
            endfor;
        %] -> sub_strs;
        sub_strs(1) <> ' ' <> word_string(hd(formula)) <> ' ' <> sub_strs(2) -> str;

    elseif hd(formula) == "all" or hd(formula) == "exists" then
        inverse_parse_formula(formula(3)) -> str;
        if islist(formula(3)) then
            if hd(formula(3)) == "/\" or hd(formula(3)) == "\/" or
                hd(formula(3)) == "->" or hd(formula(3)) == "<->" then
                '(' <> str <> ')' -> str;
            endif;
        endif;
        word_string(hd(formula)) <> ' ' <> word_string(hd(tl(formula))) <>
        ' ' <> str -> str;

    else
        'The input is not a valid formula' -> str;

    endif;
enddefine;


;;; compile('~kpl/Project/lang_manip.p');

define print_lang(lang);
    lvars lang, part, item;
    if lang then
        for part to 2 do
            if not(null(lang(part))) then
                [% for item in lang(part) do
                        front(item) >< '/' >< back(item);
                    endfor; %];
                if part == 1 then
                    line_break_spr(2, '        Predicates : ');
                else
                    line_break_spr(2, '        Functions : ');
                endif;

            else
                if part==1 then
                    'Predicates : ';
                else
                    'Functions : ';
                endif;
                <> 'None';
                ttpr();
            endif;
            nl(1);
        endfor;
    else
        ttnpr('None');
    endif;
enddefine;

define term_in_lang(term, lang, vbles) -> bool;
    lvars term, lang, vbles, bool=false, arg, arity;
    if islist(term) and not(null(term)) and (isfunc(hd(term),lang) ->> arity)
    and listlength(term)==arity+1 then
        true -> bool;
        for arg in tl(term) do
            if not(term_in_lang(arg,lang,vbles)) then
                false -> bool;
                quitloop;
            endif;
        endfor;

    elseif member(term,vbles) then
        true -> bool;
    endif;
enddefine;

define formula_in_lang(formula, lang, vbles) -> bool;
    lvars formula, lang, vbles, bool=false, arg, arity, len, connective;
    if islist(formula) and not(null(formula)) then
        listlength(formula) -> len;
        hd(formula) -> connective;

        if (ispred(connective,lang) ->> arity) and len==arity+1 then
            true -> bool;
            for arg in tl(formula) do
                if not(term_in_lang(arg,lang,vbles)) then
                    false -> bool;
                    quitloop;
                endif;
            endfor;

        elseif connective == "=" and len==3 then
            if term_in_lang(formula(2),lang,vbles)
            and term_in_lang(formula(3),lang,vbles) then
                true -> bool;
            endif;

        elseif connective == "~" and len==2 then
            if formula_in_lang(formula(2),lang,vbles) then
                true -> bool;
            endif;

        elseif (connective=="/\" or connective=="\/"
            or connective=="->" or connective=="<->") and len==3 then
            if formula_in_lang(formula(2),lang,vbles)
            and formula_in_lang(formula(3),lang,vbles) then
                true -> bool;
            endif;

        elseif (connective=="all" or connective=="exists") and len == 3 then
            if member(formula(2),vbles) and formula_in_lang(formula(3),lang,vbles) then
                true -> bool;
            endif;

        endif;

    elseif formula == "top" or formula == "bottom" then
        true -> bool;
    endif;
enddefine;

define change_lang(lang, interp, formula, assignment, vbles, instr)
        -> (lang, interp, formula, assignment, vbles);
    lvars lang, interp, formula, assignment, vbles, instr, items, part,
        count, next_item, correct_items, existing_item, other_part,
        current_part, old_lang, element, pred, func, arity, tuples,
        tuple, len_items, univ, input_item;
    vars item, item_arity, other_items;

    if lang then
        copylist(lang) -> old_lang;
    else
        [[] []] -> old_lang;
    endif;

    for part to 2 do
        ved_clear();
        tnpr('Current Language :\n');
        print_lang(lang);
        nl(1);
        if part == 1 then
            'predicate';
        else
            'function';
        endif;
        if instr then
            'Type in the new list of ' <> subscr_stack(2)
            <> 's (in the form ' <> subscr_stack(2) <> '/arity)';
            tnpr();

            tnpr('or type "u" to keep them unchanged (warning : if you use the');

            'same ' <> subscr_stack(2) <>
            ' name more than once the last definition of this';
            tnpr();

            <> ' will be the one used) :';
            tnpr();
        else
            'Type in the new list of ' <> subscr_stack(2)
            <> 's or "u" to keep them unchanged :';
            tnpr();
            erase();
        endif;

        if lang==false then
            [[] []] -> lang;
        endif;

        remove_commas(requestline('    ')) -> items;

        [%for input_item in items do
                explode(separate_symbols(input_item, [/]));
            endfor; %] -> items;

        [%for count to (listlength(items) ->> len_items) do
                items(count) -> item;

                if count < len_items then
                    items(count+1) -> next_item;
                else
                    false -> next_item;
                endif;

                if isword(item) and isstartstring("/",item) then
                    if not(isword(next_item) and isstartstring("/",next_item)) then
                        "/";
                    endif;
                else
                    item;
                endif;
            endfor;
        %] -> items;

        if not(listlength(items)==1 and
                isstartstring(uppertolower(hd(items)),'unchanged')) then

            [] -> correct_items;
            lang(3-part) -> other_part;
            while items matches [==
                    ?item:%procedure(arg); lvars arg; not(islogsymbol(arg)); endprocedure%
                    / ?item_arity:isnatural ??other_items] do

                convert_num(item) -> item;
                ;;;Updates this part of the language to avoid reuse of names.
                conspair(item,item_arity) ::
                [%for existing_item in correct_items do
                        if front(existing_item) /== item then
                            existing_item;
                        endif;
                    endfor; %] -> correct_items;

                ;;;Updates the other part of the language to avoid reuse of names.
                [%for existing_item in other_part do
                        if front(existing_item) /== item then
                            existing_item;
                        endif;
                    endfor; %] -> other_part;

                other_items -> items;
            endwhile;

            rev(correct_items) -> lang(part);
            other_part -> lang(3-part);

        endif;
    endfor;

    if interp then
        ;;;Update interp in light of changes to lang.
        ;;;First the preds.
        lang(1) -> current_part;
        [%for element in current_part do
                front(element) -> pred;
                back(element) -> arity;
                if ispred(pred,old_lang) == arity then
                    [^pred ^(interp("preds")(pred))];
                else
                    if arity == 0 then
                        [^pred ^false];
                    else
                        [^pred ^nil];
                    endif;
                endif;
            endfor; %];
        newassoc() -> interp("preds");

        ;;;Second the funcs.
        lang(2) -> current_part;
        [% for element in current_part do
                front(element) -> func;
                back(element) -> arity;
                if isfunc(func,old_lang) == arity then
                    [^func ^(interp("funcs")(func))];
                else
                    interp("univ") -> univ;
                    if arity == 0 then
                        [^func ^(hd(univ))];
                    else
                        if arity == 1 then
                            univ;
                        else
                            tuple_generator(univ,arity);
                        endif;
                            -> tuples;

                        [^func %
                            [%for tuple in tuples do
                                    [^tuple ^(hd(univ))];
                                endfor; %];
                            if arity == 1 then
                                newassoc();
                            else
                                assoc();
                            endif;
                        %];
                    endif;
                endif;
            endfor; %];
        newassoc() -> interp("funcs");
    endif;

    ;;;Now update formula,assignment and vbles in light of
    ;;;  changes made to lang.
    if formula then
        if not(formula_in_lang(formula,lang,vbles)) then
            false ->> formula;
                -> assignment;
            [] -> vbles;
        endif;
    endif;

enddefine;

;;; compile('~kpl/Project/interp_manip.p');

define print_pred_interp(pred, arity, value, univ, tab_indent);
    lvars pred, arity, value, univ, tab_indent, indiv, tuple,
        char_count, print_proc, all_indivs, my_tab;

    switchon tab_indent
    case == 1 then
        tpr;
        '    ';
    case == 2 then
        ttpr;
        '        ';
    else
        pr;
        '';
    endswitchon;
        -> my_tab;
        -> print_proc;

    if value=="undef" then

        print_proc(pred >< ' has yet to defined in this interpretation\n');

    else

        switchon arity
        case == 0 then
            print_proc('Interpretation of ' >< pred >< ' : ');
            if value then
                npr('TRUE');
            else
                npr('FALSE');
            endif;
        case == 1 then
            [% for indiv in value do
                    if member(indiv,univ) then
                        indiv;
                    endif;
                endfor; %];
            line_break_spr(tab_indent, my_tab >< 'Interpretation of ' ><
                pred >< ' : {');
            npr('}');

        case > 1 then
            [%for tuple in value do
                    true -> all_indivs;
                    for indiv in tuple do
                        if not(member(indiv,univ)) then
                            false -> all_indivs;
                            quitloop;
                        endif;
                    endfor;
                    if all_indivs then
                        tuple;
                    endif;
                endfor; %] -> value;

            [%for tuple in value do
                    `(`;
                    1 -> char_count;
                    for indiv in tuple do
                        explode(indiv);
                        `,`;
                        char_count + datalength(indiv) + 1 -> char_count;
                    endfor;
                    erase();
                    `)`;
                    consstring(char_count);
                endfor; %];
            line_break_spr(tab_indent, my_tab >< 'Interpretation of ' ><
                pred >< ' : {');
            npr('}');
        endswitchon;

    endif;

enddefine;

define print_func_interp(func, arity, value, univ, instr, partial, tab_indent);
    lvars func, arity, value, univ, instr, partial, tab_indent,
        tuple, tuples, char_count, indiv, image_indiv, print_proc,
        my_tab;

    switchon tab_indent
    case == 1 then
        tpr;
    case == 2 then
        ttpr;
        '        ' -> my_tab;
    else
        pr;
        '' -> my_tab;
    endswitchon;
        -> print_proc;

    switchon arity
    case == 0 then
        if member(value,univ) then
            print_proc('Interpretation of ' >< func >< ' : ');
            npr(value);
        else
            print_proc(func >< ' has yet to defined in this interpretation\n');
        endif;

    case > 0 then
        if instr and partial then
            print_proc('Interpretation of ' >< func ><
                ' (if for some individual i, ' >< func >< '(i)=undef\n');
        endif;

        if arity == 1 then
            univ -> tuples;
        else
            tuple_generator(univ,arity) -> tuples;
        endif;

        [%for tuple in tuples do
                explode(func);
                `(`;
                datalength(func) + 1 -> char_count;
                if arity == 1 then
                    explode(tuple);
                    char_count + datalength(tuple) -> char_count;
                else
                    for indiv in tuple do
                        explode(indiv);
                        `,`;
                        char_count + datalength(indiv) + 1 -> char_count;
                    endfor;
                    erase();
                    char_count - 1 -> char_count;
                endif;
                `)`; `=`;
                value(tuple) -> image_indiv;

                if not(member(image_indiv, univ)) then
                    "undef" -> image_indiv;
                endif;

                explode(image_indiv);
                char_count+datalength(image_indiv)+2 -> char_count;
                consstring(char_count);
            endfor; %];

        if instr and partial then
            line_break_spr(tab_indent, my_tab >< 'then ' >< func ><
                ' is not yet defined for i) : ');
        else
            line_break_spr(tab_indent, my_tab >< 'Interpretation of ' ><
                func >< ' : ');
        endif;
        nl(1);

    endswitchon;

enddefine;

define print_interp(lang, interp, instr);
    lvars lang, interp, instr, pred, func, univ, pred, func, pred_name
        func_name;
    if interp then
        line_break_spr(interp("univ") ->> univ,2, '        The universe is : ');
        nl(1);

        if not(null(lang(1))) then
            nl(1);
            for pred in lang(1) do
                print_pred_interp(front(pred) ->> pred_name,
                    back(pred), interp("preds")(pred_name), univ, 2);
            endfor;
        endif;

        if not(null(lang(2))) then
            nl(1);
            for func in lang(2) do
                print_func_interp(front(func) ->> func_name,
                    back(func), interp("funcs")(func_name), univ,
                    instr, false, 2);
            endfor;
        endif;

    else
        ttnpr('None');
    endif;
enddefine;

define pred_in_univ(pred_value, arity, univ) -> bool;
    lvars pred_value, arity, univ, bool, indiv, tuple;

    switchon arity
    case == 0 then
        true -> bool;

    case == 1 then
        true -> bool;
        for indiv in pred_value do
            if not(member(indiv, univ)) then
                false -> bool;
                quitloop;
            endif;
        endfor;

    case > 1 then
        true -> bool;
        for tuple in pred_value do
            for indiv in tuple do
                if not(member(indiv, univ)) then
                    false -> bool;
                    quitloop(2);
                endif;
            endfor;
        endfor;

    endswitchon;
enddefine;

define func_in_univ(func_value, arity, univ) -> bool;
    lvars func_value, arity, univ, bool, tuple, tuples;

    if func_value then

        switchon arity
        case == 0 then
            member(func_value, univ) -> bool;

        case > 0 then

            if arity == 1 then
                univ -> tuples;
            else
                tuple_generator(univ, arity) -> tuples;
            endif;

            true -> bool;
            for tuple in tuples do
                if not(member(func_value(tuple),univ)) then
                    false -> bool;
                    quitloop;
                endif;
            endfor;

        endswitchon;

    else
        false -> bool;
    endif;

enddefine;

define no_brackets(list) -> bool;
    lvars list, bool=true, item;
    for item in list do
        if item=="(" or item==")" then
            false -> bool;
            quitloop;
        endif;
    endfor;
enddefine;

define really_change_interp(lang, interp, assignment, vbles, instr)
        -> (interp, assignment);
    lvars lang, interp, assignment, vbles, instr, current_part, univ
        item, pred, func, arity, value, keyed_input, typed_input,
        input_item, correct_input, indiv, all_indivs, mapping,
        tuple, tuples, char_count, vble, first_element;
    vars other_input, tuple_indivs;

    if interp==false then
        newassoc([
                [preds %newassoc(
                        [%for pred in lang(1) do
                                [^(front(pred)) undef];
                            endfor; %]
                    )% ]
                [funcs %newassoc([])%]
            ]) -> interp;
    endif;

    interp("univ") -> univ;

    ;;;Update the universe.
    if univ then
        ved_clear();
        line_break_spr(univ, 1, '    The current universe is : ');
        nl(2);

        tnpr('Do you want to change the universe in this interpretation');
        tnpr('(press y or n) :');

        repeat
            vedclearinput();
            rawcharin() -> keyed_input;
            repeat 10000 times
            endrepeat;
            vedclearinput();
        quitif(keyed_input==`y` or keyed_input==`Y`
            or keyed_input==`n` or keyed_input==`N`);
        endrepeat;
    else
        `y` -> keyed_input;
    endif;

    if keyed_input==`y` or keyed_input==`Y` then
        repeat
            ved_clear();
            if univ then
                line_break_spr(univ, 1, '    The current universe is : ');
            else
                tpr('The universe has yet to be defined');
            endif;
            nl(2);

            if instr then
                tnpr('Type in the new universe of individuals (repeated individuals');
                tnpr('will only be counted once, and the universe must be');
                tnpr('non-empty) :');
            else
                tnpr('Type in the new universe of individuals :');
            endif;

            convert_nums(remove_dups(remove_commas(requestline('    '))))
                -> typed_input;

            if not(null(typed_input)) then
                typed_input -> univ;
                quitloop
            endif;
        endrepeat;

        univ -> interp("univ");

    endif;

    ;;;Update the interpretation of the predicates.
    for item in lang(1) do
        front(item) -> pred;
        back(item) -> arity;
        interp("preds")(pred) -> value;

        if value=="undef" then
            `y` -> keyed_input;
        else
            ved_clear();
            tnpr('Current Interpretation with the new universe:');
            nl(1);
            print_pred_interp(pred, arity, value, univ, 2);
            nl(1);

            tnpr('Do you want to change ' >< pred >< ' in this interpretation');
            tnpr('(press y or n) :');

            repeat
                vedclearinput();
                rawcharin() -> keyed_input;
                repeat 10000 times
                endrepeat;
                vedclearinput();
            quitif(keyed_input==`y` or keyed_input==`Y`
                or keyed_input==`n` or keyed_input==`N`);
            endrepeat;
        endif;

        if keyed_input==`y` or keyed_input==`Y` then

            repeat

                ved_clear();
                tnpr('Current Interpretation with the new universe :');
                nl(1);
                print_pred_interp(pred, arity, value, univ, 2);
                nl(1);

                switchon arity
                case == 0 then
                    tnpr('Type what you want ' >< pred ><
                        ' to be in the new interpretation,');
                    tnpr('"t" for true or "f" for false :');
                    requestline('    ') -> typed_input;
                    if listlength(typed_input)==1 then
                        uppertolower(hd(typed_input)) -> input_item;
                        if isstartstring(uppertolower(input_item),"true") then
                            true -> interp("preds")(pred);
                            quitloop;
                        elseif isstartstring(uppertolower(input_item),"false") then
                            false -> interp("preds")(pred);
                            quitloop;
                        endif;
                    endif;

                case == 1 then
                    line_break_spr(univ,1,'    The new universe is : ');
                    nl(2);
                    tnpr('Type in the individuals that you want ' >< pred ><
                        ' to be true');
                    if instr then
                        tnpr('for in the new interpretation (repeated individuals');
                        tnpr('will only be counted once, and individuals not in the');
                        tnpr('universe will be ignored) :');
                    else
                        tnpr('true for in the new interpretation :');
                    endif;

                    convert_nums(remove_dups(remove_commas(requestline('    '))))
                        -> typed_input;

                    [% for input_item in typed_input do
                            if member(input_item, univ) then
                                input_item;
                            endif;
                        endfor; %] -> interp("preds")(pred);
                    quitloop;

                case > 1 then
                    line_break_spr(univ,1, '    The new universe is : ');
                    nl(2);

                    switchon arity
                    case == 2 then
                        'pairs';
                    case == 3 then
                        'triples';
                    else
                        arity><'-tuples';
                    endswitchon;
                    'Type in the ' >< subscr_stack(2)
                    >< ' of individuals (written with round';
                    tnpr();
                    'brackets around them) that you want ' >< pred
                    >< ' to be true for';
                    tnpr();
                    if instr then
                        'in the new interpretation (repeated ' >< subscr_stack(2)
                        >< ' will only be';
                        tnpr();
                        'counted once, and ' >< subscr_stack(2)
                        >< ' containing individuals not in';
                        tnpr();
                        tnpr('the universe will be ignored) :');
                    else
                        tnpr('true for in the new interpretation :');
                    endif;
                    erase();

                    convert_nums(remove_commas(requestline('    '))) -> typed_input;

                    [%for input_item in typed_input do
                            explode(separate_symbols(input_item,[( )]));
                        endfor; %] -> typed_input;

                    remove_dups([% while typed_input matches
                                [== ( ??tuple_indivs ) ??other_input] do

                                if listlength(tuple_indivs) == arity then
                                    true -> all_indivs;
                                    for indiv in tuple_indivs do
                                        if not(member(indiv,univ)) then
                                            false -> all_indivs;
                                            quitloop;
                                        endif;
                                    endfor;
                                    if all_indivs then
                                        tuple_indivs;
                                    endif;
                                endif;
                                other_input -> typed_input;
                            endwhile; %]) -> interp("preds")(pred);
                    quitloop;

                endswitchon;

            endrepeat;

        elseif arity == 1 then
            [% for indiv in value do
                    if member(indiv,univ) then
                        indiv;
                    endif;
                endfor; %] -> interp("preds")(pred);

        elseif arity > 1 then
            [% for tuple in value do
                    true -> all_indivs;
                    for indiv in tuple do
                        if not(member(indiv,univ)) then
                            false -> all_indivs;
                            quitloop;
                        endif;
                    endfor;
                    if all_indivs then
                        tuple;
                    endif;
                endfor; %] -> interp("preds")(pred);
        endif;

    endfor;

    ;;;Update in the interpretation of the functions.
    for item in lang(2) do
        front(item) -> func;
        back(item) -> arity;
        interp("funcs")(func) -> value;

        if func_in_univ(value, arity, univ) then
            ved_clear();
            tnpr('Current Interpretation with the new universe :');
            nl(1);
            print_func_interp(func, arity, value, univ, instr, false, 2);
            nl(1);
            tnpr('Do you want to change ' >< func >< ' in this interpretation');
            tnpr('(press y or n) :');

            repeat
                vedclearinput();
                rawcharin() -> keyed_input;
                repeat 10000 times
                endrepeat;
                vedclearinput();
            quitif(keyed_input==`y` or keyed_input==`Y`
                or keyed_input==`n` or keyed_input==`N`);
            endrepeat;

        else
            `y` -> keyed_input;
        endif;

        if keyed_input==`y` or keyed_input==`Y` then

            switchon arity
            case == 0 then

                repeat

                    ved_clear();
                    tnpr('Current interpretation with the new universe :');
                    nl(1);
                    print_func_interp(func, arity, value, univ, instr, true, 2);
                    nl(1);

                    line_break_spr(univ,1, '    The new universe is : ');
                    nl(2);

                    if instr then
                        tnpr('Type in the individual you want ' >< func ><
                            ' to represent');
                        tnpr('(it must be an individual in the universe) :');
                    else
                        tnpr('Type in the individual you want ' >< func ><
                            ' to represent :');
                    endif;
                    convert_nums(requestline('    ')) -> typed_input;
                    if listlength(typed_input)==1 then
                        if member(hd(typed_input) ->> input_item, univ) then
                            input_item -> interp("funcs")(func);
                            quitloop;
                        endif;
                    endif;

                endrepeat;

            case > 0 then

                if arity == 1 then

                    if value then
                        [% for mapping in [% explode(value) %] do
                                if member(hd(mapping),univ) then
                                    mapping;
                                endif;
                            endfor; %];
                        newassoc() -> value;

                    else
                        newassoc([]) -> value;
                    endif;

                else

                    if value then
                        [% for mapping in [% explode(tl(explode(value))) %] do
                                true -> all_indivs;
                                for indiv in hd(mapping) do
                                    if not(member(indiv,univ)) then
                                        false -> all_indivs;
                                        quitloop;
                                    endif;
                                endfor;
                                if all_indivs then
                                    mapping;
                                endif;
                            endfor; %];
                        assoc() -> value;

                    else
                        assoc([]) -> value;
                    endif;

                endif;

                if arity == 1 then
                    univ -> tuples;
                else
                    tuple_generator(univ, arity) -> tuples;
                endif;

                for tuple in tuples do

                    repeat

                        ved_clear();
                        tnpr('Current Interpretation with the new universe :');
                        nl(1);
                        print_func_interp(func, arity, value, univ, instr, true, 2);
                        nl(1);

                        line_break_spr(univ,1, '    The new universe is : ');
                        nl(2);

                        `(`;
                        1 -> char_count;
                        if arity == 1 then
                            explode(tuple);
                            `)`;
                            char_count + datalength(tuple) + 1 -> char_count;
                        else
                            for indiv in tuple do
                                explode(indiv);
                                `,`;
                                char_count + datalength(indiv) + 1 -> char_count;
                            endfor;
                            erase();
                            `)`;
                        endif;
                        consstring(char_count);

                        if instr then
                            tnpr('Type in the individual you want ' >< func ><
                                subscr_stack(2) >< ' to represent');
                            tnpr('(it must be an individual in the universe) :');
                        else
                            tnpr('Type in the individual you want ' >< func ><
                                subscr_stack(2) >< ' to represent :');
                        endif;
                        erase();

                        convert_nums(requestline('    ')) -> typed_input;
                        if listlength(typed_input)==1 then
                            if member(hd(typed_input) ->> input_item, univ) then
                                input_item -> value(tuple);
                                quitloop;
                            endif;
                        endif;

                    endrepeat;

                endfor;

                value -> interp("funcs")(func);

            endswitchon;

        else

            if arity == 1 then
                [% for mapping in [% explode(value) %] do
                        if member(hd(mapping),univ) then
                            mapping;
                        endif;
                    endfor; %];
                newassoc() -> interp("funcs")(func);

            elseif arity > 1 then
                [% for mapping in [% explode(tl(explode(value))) %] do
                        true -> all_indivs;
                        for indiv in hd(mapping) do
                            if not(member(indiv,univ)) then
                                false -> all_indivs;
                                quitloop;
                            endif;
                        endfor;
                        if all_indivs then
                            mapping;
                        endif;
                    endfor; %];
                assoc() -> interp("funcs")(func);

            endif;

        endif;

    endfor;

    ;;;Update assignment in light of the changes to interp.
    if assignment then
        hd(univ) -> first_element;
        for vble in vbles do
            if not(member(assignment(vble),univ)) then
                first_element -> assignment(vble);
            endif;
        endfor;
    endif;
enddefine;

define change_interp(lang, interp, assignment, vbles, instr) -> (interp, assignment);
    lvars lang, interp, assignment, vbles, instr, keyed_input,
        extra_input, count, input_waiting, too_large, pred=1,
        func=1;

    repeat

        ved_clear();

        tnpr('Current Interpretation :\n');
        print_interp(lang, interp, instr);
        nl(1);
        tnpr('Do you want to change the current interpretation (press y or n)');
        nl(1);

        if (vvedbuffersize+3 > vedwindowlength ->> too_large) and instr then
            tnpr('Press up or down arrow keys to scroll up or down');
            tnpr('one line at a time\n');
            tnpr('Press Page Up or Page Down to scroll up or down');
            tnpr('a screenful at a time\n');
        endif;

        repeat

            vedclearinput();
            rawcharin() -> keyed_input;
            repeat 10000 times
            endrepeat;
            if (vedscr_input_waiting() ->> input_waiting) then
                [%for count to input_waiting do
                        rawcharin();
                    endfor; %] -> extra_input;
            else
                [] -> extra_input;
            endif;

            switchon keyed_input ==
            case `y` orcase `Y` then
                really_change_interp(lang, interp, assignment, vbles, instr)
                    -> (interp, assignment);
                quitloop(2);

            case `n` orcase `N` then
                quitloop(2);

            case 27 then

                switchon extra_input =
                case [91 65] orcase [79 120] then
                    ;;;Scroll up one line
                    if too_large then
                        if vedlineoffset>0 then
                            vedlineoffset -> vedline;
                        else
                            1 -> vedline;
                        endif;
                        vedcheck();
                    endif;

                case [91 66] orcase [79 114] then
                    ;;;Scroll down one line
                    if too_large then
                        if vedlineoffset + vedwindowlength <= vvedbuffersize then
                            vedlineoffset + vedwindowlength -> vedline;
                        else
                            vedlineoffset + vedwindowlength - 1 -> vedline;
                        endif;
                        vedcheck();
                    endif;

                case [91 53 126] then
                    ;;;Scroll up one screen
                    if too_large then
                        if vedlineoffset>0 then
                            vedprevscreen();
                            vedcheck();
                        endif;
                        vedlineoffset + 1 -> vedline;
                        vedcheck();
                    endif;

                case [91 54 126] then
                    ;;;Scroll down one screen
                    if too_large and
                        (vedlineoffset + vedwindowlength <= vvedbuffersize) then
                        vednextscreen();
                        vedcheck();
                    endif;
                    vedlineoffset + vedwindowlength - 1 -> vedline;
                    vedcheck();

                endswitchon;

            endswitchon;

        endrepeat;

    endrepeat;

enddefine;

;;; compile('~kpl/Project/formula_manip.p');

define change_formula(lang, interp, formula, assignment, vbles, instr)
        -> (formula, assignment, vbles);
    lvars lang, interp, formula, assignment, vbles, instr,
        keyed_input, typed_input, typed_item, parsed_input,
        altered_vbles, univ, first_element, vble;

    repeat

        ved_clear();
        tnpr('Current Formula : \n');
        if formula then
            ttnpr(inverse_parse_formula(formula));
        else
            ttnpr('None');
        endif;
        nl(1);

        tnpr('Do you want to change the current formula (press y or n) :');

        repeat
            vedclearinput();
            rawcharin() -> keyed_input;
            repeat 10000 times
            endrepeat;
            vedclearinput();
        quitif(keyed_input==`y` or keyed_input==`Y`
            or keyed_input==`n` or keyed_input==`N`);
        endrepeat;

        if keyed_input == `y` or keyed_input==`Y` then

            ved_clear();
            tnpr('Current Formula : \n');
            if formula then
                ttnpr(inverse_parse_formula(formula));
            else
                ttnpr('None');
            endif;
            nl(1);

            if instr then
                tnpr('To write formulas use the following symbols :');
                line_break_spr([
                        '/\\ for "and"' '\\/ for "or"' '-> for "implies"'
                        '<-> for "if and only if"' '~ for "not"'
                        'all for "for all"' 'exists for "there exists"'
                        'top for "top"' 'and bottom for "bottom"'
                    ], 2, false);
                nl(1);
                tnpr('Also variables be one of the letters u, v, w, x, y, or z');
                tnpr('optionally followed by a number');
                nl(1);
            endif;
            tnpr('Type in the new formula :');

            requestline('    ') -> typed_input;
            [%for typed_item in typed_input do
                    explode(separate_symbols(typed_item,
                            prioritised_list(lang)));
                endfor; %] -> typed_input;
            convert_nums(remove_commas(typed_input)) -> typed_input;
            nl(1);

            remove_dups([% for typed_item in typed_input do
                        if isvar(typed_item,lang) then
                            typed_item;
                        endif;
                    endfor; %]) -> altered_vbles;

            parse_formula(typed_input, lang, altered_vbles) -> parsed_input;

            if isstring(parsed_input) then
                tnpr('Illformed formula (press return to continue)');
                repeat
                    vedclearinput();
                    rawcharin() -> keyed_input;
                    repeat 10000 times
                    endrepeat;
                    vedclearinput();
                quitif(keyed_input==13);
                endrepeat;
            else

                parsed_input -> formula;
                altered_vbles -> vbles;
                if assignment then
                    interp("univ") -> univ;
                    hd(univ) -> first_element;
                    for vble in vbles do
                        if not(member(assignment(vble),univ)) then
                            first_element -> assignment(vble);
                        endif;
                    endfor;
                endif;
                quitloop;

            endif;

        else
            quitloop;
        endif;

    endrepeat;

enddefine;

;;; compile('~kpl/Project/assign_manip.p');

define print_assign(assignment, vbles, instr);
    lvars assignment, vbles, instr, var, char_count, indiv;
    if assignment then
        ttnpr('The variables are assigned to individuals in the universe');
        if instr then
            ttnpr('as follows (if some variable v is assigned as v |-> undef');
        endif;

        [%for var in vbles do
                explode(var);
                32; `|`; `-`; `>`; 32;
                assignment(var) -> indiv;

                if indiv==false then
                    "undef" -> indiv;
                endif;

                explode(indiv);
                datalength(var) + 5 + datalength(indiv) -> char_count;
                consstring(char_count);
            endfor; %];
        if instr then
            line_break_spr(2,
                '        then v is not yet assigned to an individual) : ');
        else
            line_break_spr(2, '        as follows : ');
        endif;
        nl(1);
    else
        ttnpr('None');
    endif;
enddefine;

define change_assign(lang, interp, assignment, vbles, instr) -> assignment;
    lvars lang, interp, assignment, vbles, instr, univ, keyed_input,
        vble, typed_input, typed_item;

    interp("univ") -> univ;

    ved_clear();
    line_break_spr(univ,1,'    The current universe is : ');
    nl(2);

    tnpr('Current Assignment :\n');
    print_assign(assignment, vbles, instr);
    nl(1);

    tnpr('Do you want to change the current assignment (press y or n),');
    if instr then
        tnpr('or delete the current assignment (press d) (this makes it');
        tnpr('so that there is no assignment of the variables) :');
    else
        tnpr('or delete the current assignment (press d) :');
    endif;

    repeat
        vedclearinput();
        rawcharin() -> keyed_input;
        repeat 10000 times
        endrepeat;
        vedclearinput();
    quitif(keyed_input==`y` or keyed_input==`Y`
        or keyed_input==`n` or keyed_input==`N`
        or keyed_input==`d` or keyed_input==`D`);
    endrepeat;

    if keyed_input==`y` or keyed_input==`Y` then

        if assignment==false then
            newassoc([]) -> assignment;
        endif;

        for vble in vbles do

            repeat

                ved_clear();
                line_break_spr(univ,1, '    The current universe is : ');
                nl(2);

                tnpr('Current Assignment :\n');
                print_assign(assignment, vbles, instr);
                nl(1);

                tnpr('Type in the individual you want the variable ' ><
                    vble >< ' to be');
                if instr then
                    tnpr('assigned to (it must be an individual in the universe) :');
                else
                    tnpr('assigned to :');
                endif;

                convert_nums(requestline('    ')) -> typed_input;
                if listlength(typed_input) == 1 then
                    if member(hd(typed_input) ->> typed_item, univ) then
                        typed_item -> assignment(vble);
                        quitloop;
                    endif;
                endif;

            endrepeat;

        endfor;

    elseif keyed_input==`d` or keyed_input==`D` then
        false -> assignment;
    endif;

enddefine;


;;; compile('~kpl/Project/model_search.p');

define check_pred(pred, set, tuples,
        lang, reduced_lang, formula, interp, univ, init_assignment, vbles, frees,
        count_interps, evaled_interps, total_interps)
        -> (model, count_interps, evaled_interps);
    lvars pred, set, tuples, lang, reduced_lang, formula, interp,
        univ, init_assignment, vbles, frees, count_interps,
        evaled_interps, total_interps, model, tuple;
    vars procedure find_model;

    set -> interp("preds")(pred);
    find_model(lang, reduced_lang, formula, interp, univ, init_assignment,
        vbles, frees, count_interps, evaled_interps, total_interps)
        -> (model, count_interps, evaled_interps);

    until model or null(tuples) do
        check_pred(pred, hd(tuples) :: set, tl(tuples) ->> tuples,
            lang, reduced_lang, formula, interp, univ, init_assignment,
            vbles, frees, count_interps, evaled_interps, total_interps)
            -> (model, count_interps, evaled_interps);
    enduntil;

enddefine;

define check_func(func, value, tuples,
        lang, reduced_lang, formula, interp, univ, init_assignment, vbles, frees,
        count_interps, evaled_interps, total_interps)
        -> (model, count_interps, evaled_interps);
    lvars func, value, tuples, lang, reduced_lang, formula, interp,
        univ, init_assignment, vbles, frees, count_interps,
        evaled_interps, total_interps, model, indiv;
    vars procedure find_model;

    if null(tuples) then
        value -> interp("funcs")(func);
        find_model(lang, reduced_lang, formula, interp, univ, init_assignment,
            vbles, frees, count_interps, evaled_interps, total_interps)
            -> (model, count_interps, evaled_interps);

    else
        for indiv in univ do
            indiv -> value(hd(tuples));
            check_func(func, value, tl(tuples),
                lang, reduced_lang, formula, interp, univ, init_assignment,
                vbles, frees, count_interps, evaled_interps, total_interps)
                -> (model, count_interps, evaled_interps);
        quitif(model);
        endfor;
    endif;
enddefine;

define find_model(lang, reduced_lang, formula, interp, univ, init_assignment,
        vbles, frees, count_interps, evaled_interps, total_interps)
        -> (model, count_interps, evaled_interps);
    lvars lang, reduced_lang, formula, interp, univ, init_assignment, vbles,
        frees, count, model, indiv, current_item, pred, func, arity,
        tuples, value, count_interps, evaled_interps, total_interps,
        percent_comp, quit_search=false;

    if null(reduced_lang(1)) and null(reduced_lang(2)) then
        if sat_all_assignments(lang, vbles, frees, interp, univ,
                init_assignment, formula) then

            interp -> model;

        else
            count_interps + 1 -> count_interps;

            while vedscr_input_waiting() do
                if rawcharin()==13 then
                    true -> quit_search;
                    quitloop;
                endif
            endwhile;

            if quit_search then
                0 -> model;
            else
                false -> model;
                if count_interps==500 then
                    evaled_interps + 500 -> evaled_interps;
                    0 -> count_interps;
                    (evaled_interps / total_interps)*100 -> percent_comp;

                    ;;;Update progress report
                    vedline - 1 -> vedline;
                    vedlinedelete();
                    1 -> vedcolumn;
                    tnpr(intof(percent_comp) >< '% complete');
                    vedscr_flush_output();

                endif;
            endif;

        endif;

    elseif null(reduced_lang(2)) then
        front(hd(reduced_lang(1)) ->> current_item) -> pred;
        back(current_item) -> arity;
        [^(tl(reduced_lang(1))) ^(reduced_lang(2))] -> reduced_lang;

        if arity == 0 then

            find_model(lang, reduced_lang, formula, interp, univ, init_assignment,
                vbles, frees, count_interps, evaled_interps, total_interps)
                -> (model, count_interps, evaled_interps);
            if not(model) then
                true -> interp("preds")(pred);
                find_model(lang, reduced_lang, formula, interp, univ, init_assignment,
                    vbles, frees, count_interps, evaled_interps, total_interps)
                    -> (model, count_interps, evaled_interps);
            endif;

        else
            if arity == 1 then
                univ;
            else
                tuple_generator(univ, arity);
            endif;
                -> tuples;

            check_pred(pred, [], tuples, lang, reduced_lang, formula, interp,
                univ, init_assignment, vbles, frees, count_interps,
                evaled_interps, total_interps)
                -> (model, count_interps, evaled_interps);
        endif;

    else
        front(hd(reduced_lang(2)) ->> current_item) -> func;
        back(current_item) -> arity;
        [^(reduced_lang(1)) ^(tl(reduced_lang(2)))] -> reduced_lang;

        if arity == 0 then

            for indiv in univ do
                indiv -> interp("funcs")(func);
                find_model(lang, reduced_lang, formula, interp, univ, init_assignment,
                    vbles, frees, count_interps, evaled_interps, total_interps)
                    -> (model, count_interps, evaled_interps);
            quitif(model);
            endfor;

        else
            if arity == 1 then
                univ;
                newassoc([]) -> value;
            else
                tuple_generator(univ, arity);
                assoc([]) -> value;
            endif;
                -> tuples;

            check_func(func, value, tuples, lang, reduced_lang, formula, interp,
                univ, init_assignment, vbles, frees, count_interps,
                evaled_interps, total_interps)
                -> (model, count_interps, evaled_interps);
        endif;

    endif;

enddefine;

define initiate_model_search(lang, formula, vbles, frees, size) -> model;
    lvars lang, formula, vbles, frees, size, model, interp, init_assignment,
        univ, count, vble, reduced_lang, item, excluded_lang, part,
        name, arity, first_indiv, tuples, tuple, total_interps=1;

    if formula == false then
        false -> model;
    else

        [%for count to size do
                "a" <> convert_num(count);
            endfor; %] -> univ;
        newassoc([
                [univ ^univ]
                [preds %newassoc([])%]
                [funcs %newassoc([])%]
            ]) -> interp;

        [%for vble in difference(vbles,frees) do
                [^vble ^(hd(univ))];
            endfor; %];
        newassoc() -> init_assignment;

        lang_used_in_formula(lang, formula) -> reduced_lang;
        lang_difference(lang, reduced_lang) -> excluded_lang;

        hd(univ) -> first_indiv;

        for part to 2 do
            for item in excluded_lang(part) do
                front(item) -> name;
                back(item) -> arity;

                if arity==0 then
                    if part==2 then
                        first_indiv -> interp("funcs")(name);
                    endif;

                else
                    if part==1 then
                        nil -> interp("preds")(name);
                    else
                        if arity==1 then
                            univ;
                        else
                            tuple_generator(univ, arity);
                        endif;
                            -> tuples;

                        [%for tuple in tuples do
                                [^tuple ^first_indiv];
                            endfor; %];
                        if arity==1 then
                            newassoc();
                        else
                            assoc();
                        endif;
                            -> interp("funcs")(name);

                    endif;
                endif;

            endfor;

            ;;;Calculate total number of interps to be evaluated.
            for item in reduced_lang(part) do
                back(item) -> arity;

                if part==1 then
                    total_interps * (2**(size**arity)) -> total_interps;
                else
                    total_interps * (size**(size**arity)) -> total_interps;
                endif;
            endfor;

        endfor;

        find_model(lang, reduced_lang, formula, interp, univ, init_assignment,
            vbles, frees, 0, 0, total_interps); erase(); erase(); -> model;

    endif;

enddefine;

define model_search(lang, formula, vbles, frees, instr) -> interp;
    lvars lang, formula, vbles, frees, instr, interp=false, model=false,
        size=1, keyed_input;

    ved_clear();
    repeat
        tnpr('Searching for model with universe of size ' >< size >< ' (press');
        tnpr('RETURN to stop searching) :');
        tnpr('0% complete');
        vedscr_flush_output();
        initiate_model_search(lang, formula, vbles, frees, size) -> model;
    quitif(model);
        vedline - 1 -> vedline;
        vedlinedelete();
        vedline - 1 -> vedline;
        vedlinedelete();
        vedline - 1 -> vedline;
        vedlinedelete();
        1 -> vedcolumn;
        tnpr('Search for model of size ' >< size >< ' : complete');
        size + 1 -> size;
    endrepeat;

    if isproperty(model) then
        ved_clear();
        tnpr('Model of the current formula :');
        nl(1);
        print_interp(lang, model, instr);
        nl(1);
        tnpr('Do you want to make this the current interpretation (press y or n)');
        nl(1);

        repeat
            vedclearinput();
            rawcharin() -> keyed_input;
            repeat 10000 times
            endrepeat;
            vedclearinput();
        quitif(keyed_input==`y` or keyed_input==`Y`
            or keyed_input==`n` or keyed_input==`N`);
        endrepeat;

        if keyed_input==`y` or keyed_input==`Y` then
            model -> interp;
        endif;

    endif;

enddefine;


;;; main program begins here


define model();
    lvars lang=false, interp=false, formula=false, assignment=false, vbles=[],
        too_large, keyed_input, extra_input, input_waiting, count, instr=true,
        univ, init_assignment, frees, vble, model;

    dlocal pop_pr_quotes = false;
    edit(vedlmr_print_in_file);
    vedsetwindow();

    repeat
        ved_clear();

        tnpr('PREDICATE LOGIC SATISFACTION CHECKER');
        nl(1);

        tnpr('Current Language :\n');
        print_lang(lang);
        nl(1);

        tnpr('Current Interpretation :\n');
        print_interp(lang, interp, instr);
        nl(1);

        tnpr('Current Formula :\n');
        if formula then
            ttnpr(inverse_parse_formula(formula));
        else
            ttnpr('None');
        endif;
        nl(1);

        tnpr('Current Assignment (optional) :\n');
        print_assign(assignment, vbles, instr);
        nl(1);

        if lang and formula then
            frees_in_formula(formula, lang) -> frees;
        endif;

        if lang and interp and formula then
            tnpr('Status :\n');
            if assignment then
                if satisfies(lang,vbles,interp,assignment,formula) then
                    ttnpr('This interpretation of the language with this assignment');
                    ttnpr('of the variables DOES satisfy the given formula');
                else
                    ttnpr('This interpretation of the language with this assignment');
                    ttnpr('of the variables does NOT satisfy the given formula');
                endif;
            else
                interp("univ") -> univ;

                [%for vble in difference(vbles, frees) do
                        [^vble ^(hd(univ))];
                    endfor; %];
                newassoc() -> init_assignment;

                if sat_all_assignments(lang,vbles,frees,interp,univ,
                        init_assignment,formula) then
                    ttnpr('This interpretation of the language DOES satisfy the');
                    ttnpr('given formula');
                else
                    ttnpr('This interpretation of the language does NOT satisfy the');
                    ttnpr('given formula');
                endif;
            endif;
            nl(1);
        endif;

        tnpr('Press 1 to change the language');
        if lang then
            tnpr('      2 to change the interpretation');
            tnpr('      3 to change the formula');
            if formula then
                if interp then
                    tnpr('      4 to change the assignment of the variables');
                    tnpr('      5 to search for a model of the current formula');
                else
                    tnpr('      4 to search for a model of the current formula');
                endif;
            endif;
        endif;
        if instr then
            tnpr('      i to reduce the instructions shown')
        else
            tnpr('      i to increase the instructions shown');
        endif;
        tnpr('      e to exit\n');

        if (vvedbuffersize+3 > vedwindowlength ->> too_large) and instr then
            tnpr('Press up or down arrow keys to scroll up or down');
            tnpr('one line at a time\n');
            tnpr('Press Page Up or Page Down to scroll up or down');
            tnpr('a screenful at a time\n');
        endif;

        repeat

            vedclearinput();
            rawcharin() -> keyed_input;
            repeat 10000 times
            endrepeat;
            if (vedscr_input_waiting() ->> input_waiting) then
                [%for count to input_waiting do
                        rawcharin();
                    endfor; %] -> extra_input;
            else
                [] -> extra_input;
            endif;

            switchon keyed_input ==
            case `e` orcase `E` then quitloop(2);
            case `i` orcase `I` then
                not(instr) -> instr;
                quitloop;
            case `1` then
                change_lang(lang, interp, formula, assignment, vbles, instr)
                    -> (lang, interp, formula, assignment, vbles);
                quitloop;
            case `2` then
                if lang then
                    change_interp(lang, interp, assignment, vbles, instr)
                        -> (interp, assignment);
                    quitloop;
                endif;
            case `3` then
                if lang then
                    change_formula(lang, interp, formula, assignment, vbles, instr)
                        -> (formula, assignment, vbles);
                    quitloop;
                endif;
            case `4` then
                if lang and formula then
                    if interp then
                        change_assign(lang, interp, assignment, vbles, instr)
                            -> assignment;
                    else
                        model_search(lang, formula, vbles, frees, instr) -> model;
                        if model then
                            model -> interp;
                        endif;
                    endif;
                    quitloop;
                endif;
            case `5` then
                if lang and interp and formula then
                    model_search(lang, formula, vbles, frees, instr) -> model;
                    if model then
                        model -> interp;
                    endif;
                    quitloop;
                endif;
            case 27 then

                switchon extra_input =
                case [91 65] orcase [79 120] then
                    ;;;Scroll up one line
                    if too_large then
                        if vedlineoffset>0 then
                            vedlineoffset -> vedline;
                        else
                            1 -> vedline;
                        endif;
                        vedcheck();
                    endif;

                case [91 66] orcase [79 114] then
                    ;;;Scroll down one line
                    if too_large then
                        if vedlineoffset + vedwindowlength <= vvedbuffersize then
                            vedlineoffset + vedwindowlength -> vedline;
                        else
                            vedlineoffset + vedwindowlength - 1 -> vedline;
                        endif;
                        vedcheck();
                    endif;

                case [91 53 126] then
                    ;;;Scroll up one screen
                    if too_large then
                        if vedlineoffset>0 then
                            vedprevscreen();
                            vedcheck();
                        endif;
                        vedlineoffset + 1 -> vedline;
                        vedcheck();
                    endif;

                case [91 54 126] then
                    ;;;Scroll down one screen
                    if too_large and
                        (vedlineoffset + vedwindowlength <= vvedbuffersize) then
                        vednextscreen();
                        vedcheck();
                    endif;
                    vedlineoffset + vedwindowlength - 1 -> vedline;
                    vedcheck();

                endswitchon;

            endswitchon;

        endrepeat;

    endrepeat;

    ved_clear();
    if vedlmr_print_in_file = 'checker output.p' then
        ved_q();
        kpl_original_output_file -> vedlmr_print_in_file;
    endif;

enddefine;
