
;;; load ~jas/Project/parser.p


define ispred(input, lang) -> arity;
    ;;; If the input is a predicate then get its 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;
    ;;; If the input is a function then get its 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;
    ;;; Checks whether the input is a variable
    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 isterm(input, lang) -> bool;
    ;;; Checks whether the input is a term
    lvars input, lang, bool=false, flag=true, item;

    if islist(input) and input/==[] then
        if isfunc(hd(input), lang)==length(tl(input)) then

            for item in tl(input) do
                if not(isterm(item, lang)) then
                    false -> flag;
                endif;
            endfor;
            flag -> bool;
        else
            false -> bool;
        endif;
    elseif isvar(input,lang)
    or isfunc(input, lang) == 0 then

        true -> bool;

    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 parse_term(input, lang) -> term;
    lvars input, lang, term;
    lvars count, open_bracs=0, first_brac_pos, brac_contents, unbrac_input=[],
    item, argument, inner_count, arity;

    if isword(input) or isinteger(input) then

        if isvar(input,lang) or 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) -> 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)->term;

            else

                'Illformed term' -> term;

            endif;

        endif;

    else

        'Illformed term : empty term' -> term;

    endif;

enddefine;

define parse_formula(input, lang) -> formula;
    lvars input, lang, 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)->left_form;
                    parse_formula(right_of,lang,)->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)->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 isvar(hd(tl(unbrac_input)),lang) then
                        parse_formula(tl(tl(unbrac_input)),lang)->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) -> 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)->left_term;
                    parse_term(unbrac_input(3),lang)->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)->formula;

                else
                    'Illformed formula' -> formula;

                endif;

            endif;

        endif;

    else

        'Illformed formula : empty formula' -> formula;

    endif;

enddefine;


;;; load ~jas/Project/rules.p


vars connectwds = [/\ \/ ~ = -> <->];
vars quantifiers = [all exists];

vars rules = [[premise] [assumption] [/\ e] [/\ i] [\/ e] [\/ i] [-> e] [-> i]
    [ass] [a] [ob] [cb] [v] [p] [~ i] [~ e] [bottom e] [~~] [= e] [= i] [all i] [all e]
    [exists e] [exists i] [open box] [close box] [carry] [var] [bye] [?]];

define ispred2(input,lang) -> boole;
    lvars input, boole=false, pair;
    vars lang;
    if islist(input) and not(input = []) then
        for pair in lang(1) do
            if front(pair) = hd(input) then
                true -> boole;
            endif;
        endfor;
    endif;
enddefine;

define isformula(input) -> boole;
    lvars boole=false, pair;
    vars var, lang, input;
    if islist(input) and not(input = []) then
        if input matches [?var ==] and (member(var,connectwds) or member(var,quantifiers)) then
            true -> boole;
        elseif ispred2(input,lang) then
            true -> boole;
        endif;
    elseif input = "bottom" or input = "top" then
        true -> boole;
    endif;
enddefine;

define assume_rule(rule,rulesused,boole) -> (rule, flag);
    lvars rule, boole, rulesused, flag;
    if rulesused = [] or (not(last(rulesused) = [open box]) and
            not(last(rulesused) = [var])) then
        if boole then
            npr('You should open a box before making an assumption');
        endif;
        true -> flag;
        [] -> rule;
    else
        [ass] -> rule;
    endif;
enddefine;

define and_e_rule(rule,formulae,boole) -> (rule,flag,list);
    lvars rule, boole, formulae, flag, list=[];
    vars lefts, rights;
    if formulae matches [== [/\ ?lefts ?rights] ==] then
        foreach [/\ ?lefts ?rights] in formulae do
            [^^list ^lefts ^rights] -> list;
        endforeach;
        rule -> rule;
    else
        if boole then
            npr('You cannot use the /\\ elimination rule here');
            npr('There is no /\\ which can be eliminated');
        endif;
        true -> flag;
        [] -> rule;
    endif;
enddefine;

define check_and_e(formula,list,rulesused) ->(formula,flag2,rulesused);
    lvars formula, list, rulesused, flag2;
    lvars ans;
    if not(member(formula,list)) then
        [] -> formula;
        npr('You cannot get this formula using /\\ e');
        npr('Do you still want to use the /\\ e rule?');
        readline() -> ans;
        until ans matches [yes] or ans matches [no] do
            npr('Please type yes or no');
            readline() -> ans;
        enduntil;
        if ans matches [yes] then
            true -> flag2;
        else
            allbutlast(1,rulesused) -> rulesused;
        endif;
    else
        formula -> formula;
        rulesused -> rulesused;
    endif;
enddefine;

define and_i_rule(rule,formulae,boole) -> (rule,flag);
    lvars formula, rule, formulae, boole, flag, num=0;
    for formula in formulae do
        if isformula(formula) then
            num + 1 -> num;
        endif;
    endfor;
    if num < 2 then
        if boole then
        npr('You need two formulae to use /\\ i');
        endif;
        [] -> rule;
        true -> flag;
    else
        rule -> rule;
    endif;
enddefine;

define check_and_i(formula,formulae,rulesused) -> (formula,flag2,rulesused);
    lvars formula, formulae, rulesused, ans, flag2;
    vars lefts, rights;
    if formula matches [/\ ?lefts ?rights] then
        if member(lefts,formulae) and member(rights,formulae) then
            formula -> formula;
            rulesused -> rulesused;
        else
            [] -> formula;
            npr('You have used tried to /\\ two formulae that don\'t exist');
            npr('Do you still want to use the /\\ i rule?');
            readline() -> ans;
            until ans matches [yes] or ans matches [no] do
                npr('Please type yes or no');
                readline() -> ans;
            enduntil;
            if ans matches [yes] then
                true -> flag2;
            else
                allbutlast(1,rulesused) -> rulesused;
            endif;
        endif;
    else
        [] -> formula;
        npr('You have not introduced an /\\');
        npr('Do you still want to use the /\\ i rule?');
        readline() -> ans;
        until ans matches [yes] or ans matches [no] do
            npr('Please type yes or no');
            readline() -> ans;
        enduntil;
        if ans matches [yes] then
            true -> flag2;
            else
            allbutlast(1,rulesused) -> rulesused;
        endif;
    endif;
enddefine;

define or_i_rule(rule,formulae,boole) -> (rule,flag);
    lvars rule, boole, formula, formulae,num=0, flag;
    for formula in formulae do
        if isformula(formula) then
            num + 1 -> num;
        endif;
    endfor;
    if num < 1 then
        if boole then
            npr('You need a formula to use \\/ i');
        endif;
        true -> flag;
        [] -> rule;
    else
        rule -> rule;
    endif;
enddefine;

define check_or_i(formula,formulae,rulesused)->(formula,flag2,rulesused);
    lvars formula, formulae, rulesused, ans, flag2;
    vars lefts, rights;
    if formula matches [\/ ?lefts ?rights] then
        if member(lefts,formulae) or member(rights,formulae) then
            formula -> formula;
            rulesused -> rulesused;
        else
            [] -> formula;
            npr('You have used tried to \\/ two formulae where neither exist already');
            npr('Do you still want to use the \\/ i rule?');
            readline() -> ans;
            until ans matches [yes] or ans matches [no] do
                npr('Please type yes or no');
                readline() -> ans;
            enduntil;
            if ans matches [yes] then
                true -> flag2;
            else
                allbutlast(1,rulesused) -> rulesused;
            endif;
        endif;
    else
        [] -> formula;
        npr('You have not introduced an \\/');
        npr('Do you still want to use the \\/ i rule?');
        readline() -> ans;
        until ans matches [yes] or ans matches [no] do
            npr('Please type yes or no');
            readline() -> ans;
        enduntil;
        if ans matches [yes] then
            true -> flag2;
        else
            allbutlast(1,rulesused) -> rulesused;
        endif;
    endif;
enddefine;

define or_e_rule(rule,formulae,boole)->(rule,flag,concls);
    lvars rule, formulae, flag, concl, boole, list=[], concls=[];
    vars lefts,rights,middle1,middle2,conc;
    if formulae matches [== [\/ ?lefts ?rights] ==] then
        foreach [\/ ^lefts ^rights] in formulae do
            [^^list [\/ ^lefts ^rights]] -> list;
        endforeach;
        foreach [\/ ?lefts ?rights] in list do
            forevery [[^lefts ??middle1 ?conc] [^rights ??middle2 ?conc]] in formulae do
                [^^concls ^conc] -> concls;
            endforevery;
            forevery [[^lefts] [^rights ??middle2 ^lefts]] in formulae do
                [^^concls ^lefts] -> concls;
            endforevery;
            forevery [[^rights] [^lefts ??middle2 ^rights]] in formulae do
                [^^concls ^rights] -> concls;
            endforevery;
        endforeach;
        if concls = [] then
            if boole then
                npr('You cannot use the \\/ e rule here since you have not derived the same ');
                npr('conclusion in two boxes, where one box starts with what appears on the ');
                npr('left of the \\/, and the other with what appears on the right');
                true -> flag;
            endif;
            [] -> rule;
        endif;
    else
        if boole then
            npr('There is no \\/ function to eliminate');
        endif;
        true -> flag;
        [] -> rule;
    endif;
enddefine;

define check_or_e(formula,rulesused,concls) -> (formula,flag2,rulesused);
    lvars formula, ans, rulesused, concls, flag2;
    if member(formula,concls) then
        formula -> formula;
        rulesused -> rulesused;
    else
        [] -> formula;
        npr('The formula you have typed does not match the one derived in the two boxes');
        npr('Do you still want to use the \\/ e rule?');
        readline() -> ans;
        until ans matches [yes] or ans matches [no] do
            npr('Please type in yes or no');
            readline() -> ans;
        enduntil;
        if ans matches [yes] then
            true -> flag2;
        else
            allbutlast(1,rulesused) -> rulesused;
        endif;
    endif;
enddefine;

define implies_i(rule, formulae,boole)->(rule, flag);
    lvars rule, formulae, flag, boole;
    vars top, middle, bottom;
    if formulae matches [== [?top:isformula ??middle ?bottom:isformula] ==]  then
    else
        if boole then
            npr('You cannot use -> i here');
            npr('You have not got from an assumption to a conclusion within a closed box');
        endif;
        [] -> rule;
        true -> flag;
    endif;
enddefine;

define check_implies_i(formula,formulae,rulesused) -> (formula,flag2,rulesused);
    lvars formula, formulae, ans, rulesused, flag2;
    vars lefts, rights, middle;
    if formula matches [-> ?lefts ?rights] then
        if formulae matches [==  [^lefts ??middle ^rights] ==] then
            formula -> formula;
            rulesused -> rulesused;
        else
            npr('You have tried to use -> i incorrectly');
            [] -> formula;
            allbutlast(1,rulesused) -> rulesused;
        endif;
    else
        [] -> formula;
        npr('You have not introduced an ->');
        npr('Do you still want to use the -> i rule?');
        readline()->ans;
        until ans matches [yes] or ans matches [no] do
            npr('Please type in yes or no');
            readline()->ans;
        enduntil;
        if ans matches [yes] then
            true -> flag2;
        else
            allbutlast(1,rulesused) -> rulesused;
        endif;
    endif;
enddefine;

define implies_e(rule, formulae,boole) -> (rule, flag);
    lvars rule, formulae, boole, flag;
    vars lefts, rights;
    if formulae matches [== [-> ?lefts ?rights] == ?lefts ==] or
        formulae matches [== ?lefts == [-> ?lefts ?rights] ==] then
    else
        if boole then
            npr('You cannot use -> e here');
        endif;
        [] -> rule;
        true -> flag;
    endif ;
enddefine;

define check_implies_e(formula,formulae,rulesused) -> (formula,flag2,rulesused);
    lvars formula, ans, formulae, rulesused, flag2;
    vars left;
    if formulae matches [== [-> ?lefts ^formula] == ?lefts ==] or
        formulae matches [== ?lefts == [-> ?lefts ^formula] ==] then
        formula -> formula;
        rulesused -> rulesused;
    else
        [] -> formula;
        npr('You have used the -> e rule incorrectly');
        npr('Check that your formula appears on the right of an implication symbol');
        npr('whose premise also occurs in the proof');
        npr('Do you still want to use this rule?');
        readline() -> ans;
        until ans matches [yes] or ans matches [no] do
            npr('Please type in yes or no');
            readline() -> ans;
        enduntil;
        if ans matches [yes] then
            true -> flag2;
        else
            allbutlast(1,rulesused) -> rulesused;
        endif;
    endif;
enddefine;

define not_i(rule,formulae,boole) -> (rule,flag);
    lvars rule, formulae, flag, boole;
    vars top, middle;
    if formulae matches [== [?top:isformula ??middle bottom] ==] then
    else
        if boole then
            npr('You canot use ~ i here');
        endif;
        [] -> rule;
        true -> flag;
    endif;
enddefine;

define check_not_i(formula,formulae,rulesused) -> (formula,flag2,rulesused);
    lvars formula, ans, formulae, rulesused, flag2;
    vars notformula, middle;
    if formula matches [~ ?notformula] then
        if formulae matches [== [^notformula ??middle bottom] ==] then
            formula -> formula;
            rulesused -> rulesused;
        else
            npr('You have used the ~ i rule incorrectly');
            npr('Check that you have derived bottom within a box that starts with the formula');
            npr('you are trying to introduce the not on');
            [] -> formula;
            npr('Do you still want to use the ~ i rule?');
            readline() -> ans;
            until ans matches [yes] or ans matches [no] do
                npr('Please type yes or no');
                readline() -> ans;
            enduntil;
            if ans matches [yes] then
                true -> flag2;
            else
                allbutlast(1,rulesused) -> rulesused;
            endif;
        endif;
    else
        [] -> formula;
        npr('You have not introduced a \'not\'');
        npr('Do you still want to use the ~ i rule?');
        readline() -> ans;
        until ans matches [yes] or ans matches [no] do
            npr('Please type yes or no');
            readline() -> ans;
        enduntil;
        if ans matches [yes] then
            true -> flag2;
        else
            allbutlast(1,rulesused) -> rulesused;
        endif;
    endif;
enddefine;

define not_e(rule,formulae,boole) -> (rule, flag);
    lvars rule, formulae, flag, boole;
    vars formula;
    if formulae matches [== [~ ?formula] == ?formula ==] or
        formulae matches [== ?formula == [~ ?formula] ==] then
    else
        if boole then
            npr('You cannot use ~ e here');
        endif;
        [] -> rule;
        true -> flag;
    endif;
enddefine;

define check_not_e(formula,formulae,rulesused) -> (formula,flag2,rulesused);
    lvars formula, ans, formulae, rulesused, flag2;
    if formula matches "bottom" then
        formula -> formula;
        rulesused -> rulesused;
    else
        [] -> formula;
        npr('You have used the ~ e rule incorrectly');
        npr('You should have derived \'bottom\'');
        npr('Do you still want to use the ~ e rule?');
        readline() -> ans;
        until ans matches [yes] or ans matches [no] do
            npr('Please type yes or no');
            readline() -> ans;
        enduntil;
        if ans matches [yes] then
            true -> flag2;
        else
            allbutlast(1,rulesused) -> rulesused;
        endif;
    endif;
enddefine;

define bottom_e(rule,formulae,boole) -> (rule,flag);
    lvars rule, formulae, boole, flag;
    vars rights;
    if formulae matches [== bottom ==] then
    else
        if boole then
            npr('You cannot use bottom e here');
        endif;
        [] -> rule;
        true -> flag;
    endif;
enddefine;

define notnot(rule,formulae,boole) -> (rule,flag);
    lvars rule, formulae, flag, boole;
    vars formula, rights;
    if formulae matches [== [~ [~ ?formula]] ==] then
    else
        if boole then
            npr('You cannot use the ~~ rule here');
        endif;
        [] -> rule;
        true -> flag;
    endif;
enddefine;

define check_notnot(formula,formulae,rulesused)->(formula,flag2,rulesused);
    lvars formula, ans, formulae, rulesused, flag2;
    vars rights;
    if formulae matches [== [~ [~ ^formula]] ==] then
        formula -> formula;
        rulesused -> rulesused;
    else
        [] -> formula;
        npr('You have used the ~~ rule incorrectly');
        npr('Check that you have deleted two nots off the front of an existing formula');
        npr('Do you really want to use the ~~ rule?');
        readline() -> ans;
        until ans matches [yes] or ans matches [no] do
            npr('Please type in yes or no');
            readline() -> ans;
        enduntil;
        if ans matches [yes] then
            true -> flag2;
        else
            allbutlast(1,rulesused) -> rulesused;
        endif;
    endif;
enddefine;

define carry(rule,formulae,boole) -> (rule,flag);
    lvars rule, formulae, flag, boole, formula;
    if formulae matches [== ?formula:isformula ==] then
    else
        if boole then
            npr('You cannot use the carry rule here');
        endif;
        [] -> rule;
        true -> flag;
    endif;
enddefine;

define check_carry(formula,formulae,rulesused) -> (formula,flag2,rulesused);
    lvars item, formula, formulae, rulesused, flag2, ans, num1=0, num2=0;
    if member(formula,formulae) then
            formula -> formula;
            rulesused -> rulesused;
    else
        [] -> formula;
        npr('The formula you have typed cannot be carried down');
        npr('Do you still want to use the carry rule?');
        readline() -> ans;
        until ans matches [yes] or ans matches [no] do
            npr('Please type in yes or no');
            readline() -> ans;
        enduntil;
        if ans matches [yes] then
            true -> flag2;
        else
            allbutlast(1,rulesused) -> rulesused;
        endif;
    endif;
enddefine;

define equals(variable) -> boole;
    lvars variable, boole;
    if variable = "=" then
        true -> boole;
    else
        false -> boole;
    endif;
enddefine;

define check_equals_i(formula,rulesused) -> (formula,flag2,rulesused);
    lvars formula, rulesused, ans, flag2;
    vars term1, term2, var, lang;
    if formula matches [?var:equals ?term1 ?term1] then
        formula -> formula;
        rulesused -> rulesused;
    else
        [] -> formula;
        npr('You have used the = introduction rule incorrectly');
        npr('Check that you did introduce an equals between two identical terms');
        npr('Do you still want to use the = introduction rule?');
        readline() -> ans;
        until ans matches [yes] or ans matches [no] do
            npr('Please type in yes or no');
            readline() -> ans;
        enduntil;
        if ans matches [yes] then
            true -> flag2;
        else
            allbutlast(1,rulesused) -> rulesused;
        endif;
    endif;
enddefine;

define funcof(formula,term) -> boole;
    lvars formula, term, boole=false, item;
    vars lang;
    if isterm(term,lang) then
        if islist(formula) then
            for item in formula do
            quitif(boole = true);
                if item = term then
                    true -> boole;
                elseif islist(item) then
                    funcof(item,term) -> boole;
                else
                endif;
            endfor;
        endif;
    endif;
enddefine;

define remove_dups(input) -> list;
    lvars item, input, list=[], output;
    for item in input do
        if member(item,list) then
        else
            [^^list ^item] -> list;
        endif;
    endfor
enddefine;

define getterms(input,list) -> list;
    lvars item input, list;
    vars lang;
    if isterm(input,lang) then
        [^^list ^input] -> list;
    elseif islist(input) then
        for item in input do
            getterms(item,list) -> list;
        endfor;
    endif;
    remove_dups(list) -> list;
enddefine;

define getvariables(input,list) -> list;
    lvars item, input, list;
    vars lang;
    if isvar(input, lang) then
        [^input] -> list
    elseif islist(input) then
        for item in input do
            [^^list ^^(getvariables(item,list))] -> list;
        endfor;
        remove_dups(list) -> list;
    endif;
enddefine;

define subterm(term,biggerterm) -> boole;
    lvars term, biggerterm, boole;
    vars item;
    if term = biggerterm then
        true -> boole;
    elseif islist(biggerterm) then
        for item in tl(biggerterm) do
            subterm(term,item) -> boole;
        quitif(boole = true);
        endfor;
    else
        false -> boole;
    endif;
enddefine;

define free(term,formula) -> boole;
    lvars term, formula, boole, termvars;
    vars var, x, rest, formula1, formula2;
    getvariables(term,[]) -> termvars;
    if formula matches [all ?x ?rest] or formula matches [exists ?x ?rest] then
        if member(x,termvars) then
            false -> boole;
        else
            free(term,rest) -> boole;
        endif;
    elseif formula = "top" or formula = "bottom" then
        false -> boole;
    elseif ispred2(formula,lang) or formula matches [?var:equals ==] then
        for item in tl(formula) do
            subterm(term,item) -> boole;
        quitif(boole = true);
        endfor;
    elseif formula matches [~ ?formula1] then
        free(term,formula1) -> boole;
    elseif formula matches [?item ?formula1 ?formula2] and member(item,connectwds) then
        free(term,formula1) or free(term,formula2) -> boole;
    else
        false -> boole;
    endif;
enddefine;

;;; term1 is free for term2 in formula
define freefor(term1,term2,formula) -> boole;
    lvars term1, term2, formula, boole=true, term1vars, term2vars;
    vars item, x, rest, formula1, formula2;
    getvariables(term1,[]) -> term1vars;
    getvariables(term2,[]) -> term2vars;
    if formula matches [?item ?x ?rest] and member(item,quantifiers) then
        if member(x,term2vars) then
            true -> boole;
        elseif member(x,term1vars) and free(term2,rest) then
            false -> boole;
        endif;
    elseif formula matches [~ ?formula1] then
        freefor(term1,term2,formula1) -> boole;
    elseif formula matches [?item ?formula1 ?formula2] and member(item,connectwds) then
        freefor(term1,term2,formula1) and freefor(term1,term2,formula2) -> boole;
    endif;
enddefine;

;;; subst sterm for oldterm in wholeterm
define termsubst(sterm, oldterm, wholeterm) -> term;
    lvars sterm, oldterm, wholeterm, term, list=[];
    vars item;
    if subterm(oldterm,wholeterm) then
        if oldterm = wholeterm then
            sterm -> term;
        else
            for item in tl(wholeterm) do
                [^^list ^(termsubst(sterm,oldterm,item))] -> list;
            endfor;
            [^(hd(wholeterm)) ^^list] -> term;
        endif;
    else
        wholeterm -> term
    endif;
enddefine;

;;;subst sterm for oldterm in formula
define subst(sterm,oldterm,formula) -> newformula;
    lvars sterm, oldterm, formula, newformula, termvars, list=[];
    vars item, var, term1, x, term2, formula1, formula2;
    if formula = "top" or formula = "bottom" then
        formula -> newformula;
    elseif ispred2(formula,lang) then
        for item in tl(formula) do
            [^^list ^(termsubst(sterm,oldterm,item))] -> list;
        endfor;
        [^(hd(formula)) ^^list] -> newformula;
    elseif formula matches [?var:equals ?term1 ?term2] then
        [^var ^(termsubst(sterm,oldterm,term1)) ^(termsubst(sterm,oldterm,term2))] -> newformula;
    elseif formula matches [~ ?formula1] then
        [~ ^(subst(sterm,oldterm,formula1))] -> newformula;
    elseif formula matches [?var ?formula1 ?formula2] and member(var,connectwds) then
        [^var ^(subst(sterm,oldterm,formula1)) ^(subst(sterm,oldterm,formula2))] -> newformula;
    elseif formula matches [?var ?x ?formula1] and member(var,quantifiers) then
        getvariables(oldterm,[]) -> termvars;
        if member(x,termvars) then
            formula -> newformula;
        else
            [^var ^x ^(subst(sterm,oldterm,formula1))] -> newformula;
        endif;
    endif;
enddefine;

define var_rule(rule,rulesused,boole) -> (rule, flag);
    lvars rule, rulesused, flag, boole;
    if rulesused = [] or not(last(rulesused) = [open box]) then
        if boole then
            npr('You should open a box before introducing a variable');
        endif;
        true -> flag;
        [] -> rule;
    else
        [var] -> rule;
    endif;
enddefine;

define isvar2(input) -> boole;
    lvars boole, input;
    vars lang;
    if islist(input) and not(input = []) then
        if length(input) = 1 and isvar(hd(input),lang) then
            true -> boole;
        else
            false -> boole;
        endif;
    else
        false -> boole;
    endif;
enddefine;

define check_var_rule(formula,formulae,rulesused) -> (formula,flag2,rulesused);
    lvars formula, boole = false, flag2,variable, ans, rulesused;
    vars form;
    if isvar2(formula) then
        for form in formulae do
            if funcof(form,hd(formula)) then
                true ->boole
            endif;
        endfor;
        if boole = false then
            formula -> formula;
            rulesused -> rulesused;
        else
            [] -> formula;
            npr('The variable already appears in your proof');
            npr('Do you still want to use var rule?');
            readline() -> ans;
            until ans matches [yes] or ans matches [no] do
                npr('Please type in yes or no');
                readline() -> ans;
            enduntil;
            if ans matches [yes] then
                true -> flag2;
            else
                allbutlast(1,rulesused) -> rulesused;
            endif;
        endif;
    else
        [] -> formula;
        npr('You did not type in a variable');
        npr('Do you still want to use var rule?');
        readline() -> ans;
        until ans matches [yes] or ans matches [no] do
            npr('Please type in yes or no');
            readline() -> ans;
        enduntil;
        if ans matches [yes] then
            true -> flag2;
        else
            allbutlast(1,rulesused) -> rulesused;
        endif;
    endif;
enddefine;

define all_i(rule,formulae,boole) -> (rule,flag,list);
    lvars rule, formulae, flag, boole,list=[];
    vars var, middle, formula;
    foreach [?var:isvar2 ??middle ?formula:isformula] in formulae do
        if funcof(formula,hd(var)) then
            [^^list [^var ^^middle ^formula]] -> list;
        endif;
    endforeach;
    if list = [] then
        if boole then
            npr('You cannot use the all introduction rule here');
        endif;
        [] -> rule;
        true -> flag;
    endif;
enddefine;

define check_all_i(formula,list,rulesused) -> (formula,flag2,rulesused);
    lvars formula, list, ans, flag=false, rulesused, flag2;
    vars var, rest, var2, middle form;
    if formula matches [all ?var ?rest] and funcof(rest,var) then
        foreach [?var2 ??middle ?form] in list do
            if subst(hd(var2),var,rest) = form then
                true -> flag;
            endif;
        endforeach;
        if flag = true then
            formula -> formula;
            rulesused -> rulesused;
        else
            [] -> formula;
            npr('You have not replaced the variables correctly');
            npr('Do you still want to use the = introduction rule?');
            readline() -> ans;
            until ans matches [yes] or ans matches [no] do
                npr('Please type in yes or no');
                readline() -> ans;
            enduntil;
            if ans matches [yes] then
                true -> flag2;
            else
                allbutlast(1,rulesused) -> rulesused;
            endif;
        endif
    else
        [] -> formula;
        npr('You have not introduced the all correctly');
        npr('Check that you have introduced an all and that the formula is');
        npr('a function of the introduced variable');
        npr('Do you still want to use the all introduction rule?');
        readline() -> ans;
        until ans matches [yes] or ans matches [no] do
            npr('Please type in yes or no');
            readline() -> ans;
        enduntil;
        if ans matches [yes] then
            true -> flag2;
        else
            allbutlast(1,rulesused) -> rulesused;
        endif;
    endif;
enddefine;

define all_e(rule,formulae,boole) -> (rule,flag,list);
    lvars rule, formulae, flag, boole, list=[];
    vars var, form;
    foreach [all ?var ?form] in formulae do
        [^^list [^form ^var]] -> list;
    endforeach;
    if list = [] then
        if boole then
            npr('There is not a for all formula that you can eliminate');
        endif;
        true -> flag;
        [] -> rule;
    endif;
enddefine;

define check_all_e(formula,list,rulesused) -> (formula,flag2,rulesused);
    lvars formula, list, ans, rulesused, terms, formula, flag2, formulas=[];
    vars term;

    getterms(formula,[]) -> terms;
    for term in terms do
        foreach [?form ?var] in list do
            if freefor(term,var,form) then
                [^^formulas ^(subst(term,var,form))] -> formulas;
            endif;
        endforeach
    endfor;
    if terms = [] then
        foreach [?form ?var] in list do
            if formula = form then
                [^^formulas ^formula] -> formulas
            endif;
        endforeach;
    endif;
    if formulas = [] then
        [] -> formula;
        if terms = [] then
            npr('You derived the wrong formula');
        else
            pr('The term you substituted in was not free for ');pr(var);npr(' in the formula');
        endif;
        npr('Do you still want to use the for all elimination rule?');
        readline() -> ans;
        until ans matches [yes] or ans matches [no] do
            npr('Please type in yes or no');
            readline() -> ans;
        enduntil;
        if ans matches [yes] then
            true -> flag2;
        else
            allbutlast(1,rulesused) -> rulesused;
        endif;
    elseif member(formula,formulas) then
        formula -> formula;
        rulesused -> rulesused;
    else
        [] -> formula;
        npr('You have used the for all elimination rule incorrectly');
        npr('Do you still want to use the for all elimination rule?');
        readline() -> ans;
        until ans matches [yes] or ans matches [no] do
            npr('Please type in yes or no');
            readline() -> ans;
        enduntil;
        if ans matches [yes] then
            true -> flag2;
        else
            allbutlast(1,rulesused) -> rulesused;
        endif;
    endif;
enddefine;

define exists_i(rule,formulae,boole) -> (rule,flag,formlist);
    lvars rule, formulae, boole, flag, formlist= [];
    vars  item;
    for item in formulae do
        if isformula(item) then
            [^^formlist ^item] -> formlist;
        endif;
    endfor;
    if formlist = [] then
        [] -> rule;
        true -> flag;
        if boole then
            npr('You need a formula to be able to use exists i');
        endif;
    else
        rule -> rule;
    endif;
enddefine;

define check_exists_i(formula,formlist,rulesused) -> (formula,flag2,rulesused);
    lvars formula, ans, formlist, terms, boole = false, rulesused, flag2, flag = false;
    vars var, formula2, lang;
    if formula matches [exists ?var ?formula2] and isvar(var,lang) then
        for form in formlist do
            getterms(form,[]) -> terms;
            for term in terms do
                if freefor(term,var,formula2) then
                    if subst(term,var,formula2)= form then
                        true -> boole;
                    endif;
                endif;
            endfor;
        endfor;
        if boole = true then
            formula -> formula;
        else
            [] -> formula;
            npr('You have used the exists introduction rule incorrectly');
            npr('Check that you have substituted the variables correctly');
            npr('Do you still want to use the exists introduction rule?');
            true ->flag;
        endif;
    else
        [] -> formula;
        npr('You have used the exists introduction rule incorrectly');
        npr('The formula you entered was not of the form \' exists variable formula \'');
        npr('Do you still want to use the exists introduction rule;?');
        true -> flag;
    endif;
    if flag = true then
        readline() -> ans;
        until ans matches [yes] or ans matches [no] do
            npr('Please type in yes or no');
            readline() -> ans;
        enduntil;
        if ans matches [yes] then
            true -> flag2;
        else
            allbutlast(1,rulesused) -> rulesused;
        endif;
    endif;
enddefine;

define exists_e(rule,formulae,boole) -> (rule,flag,list);
    lvars rule, formulae, flag, boole, list=[], concs=[];
    vars var, form, vble, conc, formula;
    if formulae matches [== [?vble:isvar2 ?formula:isformula == ?conc:isformula] ==] then
        foreach [?vble:isvar2 ?formula:isformula == ?conc:isformula] in formulae do
            if formulae matches [== [exists ?var ?form] ==] and funcof(form,var) then
                foreach [exists ?var ?form] in formulae do
                    if funcof(form,var) then
                        if subst(hd(vble),var,form) = formula then
                            [^^list ^conc] -> list;
                        endif;
                    endif;
                endforeach;
            else
                if boole then
                    npr('There is no exists symbol which can be eliminated');
                endif;
                [] -> rule;
                true -> flag;
                quitloop();
            endif;
        endforeach;
        for conc in list do
            if funcof(conc,vble) then
            else
                [^^concs ^conc] -> concs;
            endif;
        endfor;
        if concs = [] then
            if boole then
                npr('You cannot use the exists elimination rule');
            endif;
            [] -> rule;
            true -> flag;
        endif;
    else
        if boole then
            npr('You cannot use the exists elimination rule');
            npr('There isn\'t a closed box staring with a variable and ending with a formula');
        endif;
        [] -> rule;
        true -> flag;
    endif;
enddefine;

define check_exists_e(formula,list,rulesused) -> (formula,flag2,rulesused);
    lvars formula, ans, list, rulesused, flag2;
    if member(formula,list) then
        formula -> formula;
        rulesused -> rulesused;
    else
        [] -> formula;
        npr('The formula you have typed was not one derived in a box');
        npr('Do you still want to use the exists e rule?');
        readline() -> ans;
        until ans matches [yes] or ans matches [no] do
            npr('Please type yes or no');
            readline() -> ans;
        enduntil;
        if ans matches [yes] then
            true -> flag2;
        else
            allbutlast(1,rulesused) -> rulesused;
        endif;
    endif;
enddefine;

define check_term(t1,t2,conc_term,form_term,bounds) -> boole;
    lvars t1, t2, conc_term, form_term, bounds, boole=false,count;
    lvars term_vars,conc_func,form_func,conc_args,form_args,conc_len,form_len;
    vars var;
    if conc_term = form_term then
        true -> boole;
    elseif conc_term = t2 and form_term = t1 then
        [^^(getvariables(conc_term,[])) ^^(getvariables(form_term,[]))] -> term_vars;
        true -> boole;
        for var in term_vars do
            if member(var,bounds) then
                false -> boole;
            endif;
        quitif(boole = false);
        endfor;
    else
        if islist(conc_term) and islist(form_term) then
            hd(conc_term) -> conc_func;
            hd(form_term) -> form_func;
            tl(conc_term) -> conc_args;
            tl(form_term) -> form_args;
            length(conc_args) -> conc_len;
            length(form_args) -> form_len;
            if conc_func == form_func and conc_len == form_len then
                true -> boole;
                for count to conc_len do
                    check_term(t1,t2,conc_args(count),form_args(count),bounds) -> boole;
                quitif(boole = false);
                endfor;
            endif;
        endif;
    endif;
enddefine;

define check(t1,t2,conc,form,bounds) -> boole;
    lvars t1, t2, conc, form, bounds, boole=false;
    lvars conc_conn, form_conn, conc_args,form_args,conc_len,form_len;
    vars count;
    if conc = "top" or conc = "bottom" then
        form = conc -> boole;
    else
        hd(conc) -> conc_conn;
        hd(form) -> form_conn;
        tl(conc) -> conc_args;
        tl(form) -> form_args;
        length(conc_args) -> conc_len;
        length(form_args) -> form_len;
        if conc_conn = form_conn and conc_len == form_len then
            if ispred2([^(conc_conn)],lang) or conc_conn = "=" then
                true -> boole;
                for count to conc_len do
                    check_term(t1,t2,conc_args(count),form_args(count),bounds) -> boole;
                quitif(boole = false);
                endfor;
            elseif conc_conn = "~" then
                check(t1,t2,conc_args(1),form_args(1),bounds) -> boole;
            elseif member(conc_conn,connectwds) then
                check(t1,t2,conc_args(1),form_args(1),bounds) and
                check(t1,t2,conc_args(2),form_args(2),bounds) -> boole;
            elseif member(conc_conn,quantifiers) and conc_args(1) = form_args(1) then
                [^(conc_args(1)) ^^bounds] -> bounds;
                check(t1,t2,conc_args(2),form_args(2),bounds) -> boole;
            endif;
        endif;
    endif;
enddefine;

define equals_e(rule,formulae,boole) -> (rule,flag,equalterms,formulas);
    lvars rule, formula,formulas = [], boole, term, flag, equalterms = [];
    vars var, term1, term2;
    foreach [?var:equals ?term1 ?term2] in formulae do
        if not(member([^term1 ^term2],equalterms)) then
            [^^equalterms [^term1 ^term2]] -> equalterms;
        endif;
    endforeach;
    if equalterms = [] then
        if boole then
            npr('You cannot use the = elimination rule');
            npr('There are no two different terms that are declared as being equal to one another');
        endif;
        true -> flag;
        [] -> rule;
    else
        foreach [?term1 ?term2] in equalterms do
            for formula in formulae do
                if formula matches [?var:equals ^term1 ^term2] then
                else
                    if isformula(formula) then
                        if funcof(formula,term1) then
                            [^^formulas ^formula] -> formulas;
                        endif;
                    endif;
                endif;
            endfor;
        endforeach;
        if formulas = [] then
            if boole then
                npr('You cannot use the = elimination rule');
                npr('There is no formula which is a function of a term, ie f(t1), where the term is also');
                npr('defined as being equal to another term, ie t1 = t2, (not t2 = t1).');
            endif;
            true -> flag;
            [] -> rule;
        else
            rule -> rule;
        endif;
    endif;
enddefine;

define check_equals_e(formula,formulae,equalterms,rulesused) -> (formula,flag2,rulesused);
    lvars formulae, terms, equalterms, rulesused, formula, flag2;
    lvars bounds, boole, ans;
    vars term1, term2, oldformula;
    getterms(formula, []) -> terms;
    for term2 in terms do
        foreach  [?term1 ^term2] in equalterms do
            for oldformula in formulae do
                check(term1,term2,formula,oldformula,[]) -> boole;
            quitif(boole = true);
            endfor;
        quitif(boole = true);
        endforeach;
    quitif(boole = true);
    endfor;
    if boole then
    else
        npr('You have used the = elimination rule incorrectly');
        [] -> formula;
        npr('Do you still want to use the = elimination rule?');
        readline() -> ans;
        until ans matches [yes] or ans matches [no] do
            npr('Please type in yes or no');
            readline() -> ans;
        enduntil;
        if ans matches [yes] then
            true -> flag2;
        else
            allbutlast(1,rulesused) -> rulesused;
        endif;
    endif;
enddefine;

define help(boxes,rulesused,facts);
    lvars boxes, rules = [[premise] [= i] [open box]], rule, list, rulesused,flag;
    lvars concls, formulas, facts, equalterms;
    assume_rule([assumption],rulesused,false) -> (rule, flag);
    if rule = [] then
    else
        [^^rules [assumption]] -> rules;
    endif;
    and_e_rule([/\ e],facts,false) -> (rule,flag,list);
    if rule = [] then
    else
        [^^rules ^rule] -> rules;
    endif;
    and_i_rule([/\ i],facts,false) -> (rule,flag);
    if rule = [] then
    else
        [^^rules ^rule] -> rules;
    endif;
    or_i_rule([\/ i],facts,false) -> (rule,flag);
    if rule = [] then
    else
        [^^rules ^rule] -> rules;
    endif;
    or_e_rule([\/ e],facts,false) -> (rule,flag,concls);
    if rule = [] then
    else
        [^^rules ^rule] -> rules;
    endif;
    implies_i([-> i],facts,false) -> (rule,flag);
    if rule = [] then
    else
        [^^rules ^rule] -> rules;
    endif;
    implies_e([-> e],facts,false) -> (rule,flag);
    if rule = [] then
    else
        [^^rules ^rule] -> rules;
    endif;
    not_i([~ i],facts,false) -> (rule,flag);
    if rule = [] then
    else
        [^^rules ^rule] -> rules;
    endif;
    not_e([~ e],facts,false) -> (rule,flag);
    if rule = [] then
    else
        [^^rules ^rule] -> rules;
    endif;
    bottom_e([bottom e],facts,false) -> (rule,flag);
    if rule = [] then
    else
        [^^rules ^rule] -> rules;
    endif;
    notnot([~~],facts,false) -> (rule,flag);
    if rule = [] then
    else
        [^^rules ^rule] -> rules;
    endif;
    carry([carry],facts,false) -> (rule,flag);
    if rule = [] then
    else
        [^^rules ^rule] -> rules;
    endif;
    equals_e([= e],facts,false) -> (rule,flag,equalterms,formulas);
    if rule = [] then
    else
        [^^rules ^rule] -> rules;
    endif;
    var_rule([var],rulesused,false) -> (rule,flag);
    if rule = [] then
    else
        [^^rules ^rule] -> rules;
    endif;
    all_i([all i],facts,false) -> (rule,flag,list);
    if rule = [] then
    else
        [^^rules ^rule] -> rules;
    endif;
    all_e([all e],facts,false) -> (rule,flag,list);
    if rule = [] then
    else
        [^^rules ^rule] -> rules;
    endif;
    exists_i([exists i],facts,false) -> (rule,flag,list);
    if rule = [] then
    else
        [^^rules ^rule] -> rules;
    endif;
    exists_e([exists e],facts,false) -> (rule,flag,list);
    if rule = [] then
    else
        [^^rules ^rule] -> rules;
    endif;
    if boxes > 0 then
        [^^rules [close box]] -> rules;
    endif;
    if rulesused = [] then
    elseif last(rulesused) = [open box] then
        [[var] [assumption] [close box]] -> rules;
    endif;
    nl(1);
    npr('You can use any of the following rules:');
    for rule in rules do
        if length(rule) = 1 then
            npr(hd(rule));
        else
            spr(hd(rule));npr(last(rule))
        endif;
    endfor;
    nl(1);
enddefine;

;;; =======================

;;; mail program begins here



define rparse_term(input) -> output;
    lvars input, output, item, string='', count;
    if islist(input) then
        if length(input) = 1 then
            hd(input) -> output;
        else
            for count from 2 to length(input) - 1 do
                string >< rparse_term(input(count)) >< ', ' -> string;
            endfor;
            hd(input) >< '(' >< string >< rparse_term(last(input)) >< ')' -> output;
        endif;
    else
        input -> output;
    endif;
enddefine;

define rparse_pred(input) -> output;
    lvars input, output, string= '', count;
    if length(input) = 1 then
        hd(input) -> output;
    else
        for count from 2 to length(input) - 1 do
            string >< rparse_term(input(count)) >< ', ' -> string;
        endfor;
        hd(input) >< '(' ><string >< rparse_term(last(input)) >< ')' -> output;
    endif;
enddefine;

define rparse_formula(input) -> output;
    lvars input, output, lefts, rights;;
    vars var, formula1, formula2, var1, var2, lang, form1, form2;
    if input = "top" then
        'top' -> output;
    elseif input = "bottom" then
        'bottom' -> output;
    elseif ispred2(input,lang) then
        rparse_pred(input) -> output;
    elseif isvar2(input) then
        hd(input) -> output;
    elseif input matches [~ ?formula1] then
        if formula1 matches [?var ?form1 ?form2] and member(var,connectwds) then
            '~(' >< rparse_formula(formula1) >< ')' -> output;
        else
            '~' >< rparse_formula(formula1) -> output;
        endif;
    elseif input matches [?var:equals ?form1 ?form2] then
        rparse_term(form1) >< ' = ' >< rparse_term(form2) -> output;
    elseif input matches [?var:equals ?formula1 ?formula2] then
        rparse_formula(formula1) >< ' = ' >< rparse_formula(formula2) -> output;
    elseif input matches [?var ?formula1 ?formula2] and member(var,connectwds)then
        if var = [/\] then
            [/\\] -> var;
        elseif var = [\/] then
            [\\/] -> var;
        endif;
        if formula1 matches [?var1 ?form1 ?form2] and member(var1,connectwds) then
            if var = "->" and var1 = "->" then
                '(' >< rparse_formula(formula1) >< ')' -> lefts;
            elseif var = var1 then
                rparse_formula(formula1) -> lefts;
            elseif var = "->" and not(var1 = "->") then
                rparse_formula(formula1) -> lefts;
            else
                '(' >< rparse_formula(formula1) >< ')' -> lefts;
            endif;
        else
            rparse_formula(formula1) -> lefts;
        endif;
        if formula2 matches [?var2 ?form1 ?form2] and member(var2,connectwds) then
            if var = "->" and var2 = "->" then
                '(' >< rparse_formula(formula2) >< ')' -> rights;
            elseif var = var2 then
                rparse_formula(formula2) -> lefts;
            elseif var = "->" and not(var2 = "->") then
                rparse_formula(formula2) -> rights;
            else
                '(' >< rparse_formula(formula2) >< ')' -> rights;
            endif;
        else
            rparse_formula(formula2) -> rights;
        endif;
        lefts ><' '>< var ><' '>< rights -> output;
    elseif input matches [?var1 ?var2 ?formula1] then
        if formula1 matches [?var ?form1 ?form2] and member(var,connectwds) then
            '(' >< rparse_formula(formula1) >< ')' -> rights;
        else
            rparse_formula(formula1) -> rights;
        endif;
        var1 >< ' ' >< var2 >< ' ' >< rights -> output;
    else
        npr('I have not got a clue');
    endif
enddefine;

define glength(list) -> num;
    lvars list, lnum=0, num=0;
    until list = [] do
        if hd(list) = [open box] or hd(list) = [close box] then
        else
            length(rparse_formula(hd(list))) -> lnum;
            if lnum > num then
                lnum -> num;
            endif;
        endif;
        tl(list) -> list;
    enduntil;
enddefine;

define print(item,n);
    lvars item, n;
    repeat n times
        pr(item);
    endrepeat;
enddefine;

define proofbox(formulae,rulesused,complete,conc);
    lvars num, num1=0, rulesused, num2=0, numf, formulae, formula, count, complete, boxes = 0;
    glength(formulae) -> num;
    num + 2 -> num;
    for formula in formulae do
        if formula = [open box] then
            num2 + 1 -> num2;
            if num2 > num1 then
                num2 -> num1;
            endif;
        elseif formula = [close box] then
            num2 - 1 -> num2
        endif;
    endfor;
    edit(vedlmr_print_in_file);
    ved_clear();
    if complete then
        nl(1); npr('Proof: ');
    else
        nl(1); npr('Proof so far: ');
    endif;
    until formulae = [] do
        if hd(formulae) = [open box] then
            boxes + 1 -> boxes;
            if boxes > 1 then
                print("|",boxes-1);sp(1);print("_",num+num1-boxes+num1-boxes);sp(1);print("|",boxes-1);nl(1);
                print("|",boxes);sp(num+num1+num1-boxes-boxes);print("|",boxes);nl(1);
            else
                sp(boxes);print("_",num+num1-boxes+num1-boxes);nl(1);
                print("|",boxes);sp(num+num1+num1-boxes-boxes);print("|",boxes);nl(1);
            endif;
        elseif hd(formulae) = [close box] then
            print("|",boxes);print("_",num+num1+num1-boxes-boxes);print("|",boxes);nl(1);
            boxes - 1 -> boxes;
        else
            num - 1 - length(rparse_formula(hd(formulae))) -> numf;
            if boxes > 0 then
                print("|",boxes);sp(1);sp(num1-boxes);pr(rparse_formula(hd(formulae)));sp(numf);
                sp(num1-boxes);print("|",boxes);sp(1);
                if length(hd(rulesused)) = 1 then
                    npr(hd(hd(rulesused)))
                else
                    spr(hd(hd(rulesused)));npr(last(hd(rulesused)));
                endif;
            else
                sp(1);sp(num1-boxes);pr(rparse_formula(hd(formulae)));sp(numf+num1+1);
                if length(hd(rulesused)) = 1 then
                    npr(hd(hd(rulesused)))
                else
                    spr(hd(hd(rulesused)));npr(last(hd(rulesused)));
                endif;
            endif;
        endif;
        tl(formulae) -> formulae;
        tl(rulesused) -> rulesused;
    enduntil;
    if complete then
    else
        nl(1);
        npr('Conclusion: ');
        tabs(1);npr(rparse_formula(conc));
    endif;
enddefine;

define interface(facts, newfacts,flag,flag2,topflag,boxes,rulesused,formulae,conc,lang)->(proof,formulae,rulesused,boxes,topflag);
    lvars newfacts, facts, list, topflag = false, rulesused, rule, newformula, formula;
    lvars subproof, flag, flag2, concls, proof, equalterms, formulas, conc, lang;
    until rule = [close box] and boxes > 0 do
    quitif(topflag = true);
        false -> flag;
        unless flag2 == true then
            npr('Please type in what rule you wish to use');
            readline() -> rule;
            if not(member(rule,rules)) then
                until member(rule, rules) do
                    npr('Sorry I do not understand what rule you mean');
                    npr('Please try again');
                    readline() -> rule;

                enduntil;
            endif;
            if rule = [close box] or rule = [cb] then
                if boxes > 0 then
                    [close box] -> rule;
                else
                    [] -> rule;
                    npr('There is no box to close');
                endif;
                true -> flag;
            elseif rule = [?] then
                help(boxes,rulesused,facts);
                true -> flag;
                [] -> rule;
            elseif rule = [bye] then
                true -> topflag;
                true -> flag;
            elseif rule = [premise] or rule = [p] then
                [premise] -> rule;
            elseif rule = [= i]  then
            elseif rule = [assumption] or rule = [ass] or rule = [a] then
                assume_rule(rule,rulesused,true) -> (rule, flag);
            elseif rule = [open box] or rule = [ob] then
                if rulesused = [] or not(last(rulesused) = [open box]) then
                    [open box] -> rule;
                    boxes + 1 -> boxes;
                    [^^rulesused ^rule] -> rulesused;
                    [^^formulae ^rule] -> formulae;
                    npr('You should type in a var or an assumption next');
                    interface(facts, [], flag, flag2,topflag,boxes,rulesused,formulae,conc,lang) ->(subproof,formulae,rulesused,boxes,topflag);
                    true -> flag;
                    [^^facts [^^subproof]] -> facts;
                    [^^newfacts [^^subproof]] -> newfacts;
                else
                    npr('You cannot open one box immediately after opening another');
                    [] -> rule;
                    true -> flag;
                endif;
            quitif(topflag = true);
            elseif rule = [/\ e] then
                and_e_rule(rule,facts,true) -> (rule,flag,list);
            elseif rule = [/\ i] then
                and_i_rule(rule,facts,true) -> (rule,flag);
            elseif rule = [\/ i] then
                or_i_rule(rule,facts,true) -> (rule,flag);
            elseif rule = [\/ e] then
                or_e_rule(rule,facts,true) -> (rule,flag,concls);
            elseif rule = [-> i] then
                implies_i(rule,facts,true) -> (rule,flag);
            elseif rule = [-> e] then
                implies_e(rule,facts,true) -> (rule,flag);
            elseif rule = [~ i] then
                not_i(rule,facts,true) -> (rule,flag);
            elseif rule = [~ e] then
                not_e(rule,facts,true) -> (rule,flag);
            elseif rule = [bottom e] then
                bottom_e(rule,facts,true) -> (rule,flag);
            elseif rule = [~~] then
                notnot(rule,facts,true) -> (rule,flag);
            elseif rule = [carry] then
                carry(rule,facts,true) -> (rule,flag);
            elseif rule = [= e] then
                equals_e(rule,facts,true) -> (rule,flag,equalterms,formulas);
            elseif rule = [var] or rule = [v] then
                var_rule(rule,rulesused,true) -> (rule,flag);
            elseif rule = [all i] then
                all_i(rule,facts,true) -> (rule,flag,list);
            elseif rule = [all e] then
                all_e(rule,facts,true) -> (rule,flag,list);
            elseif rule = [exists i] then
                exists_i(rule,facts,true) -> (rule,flag,list);
            elseif rule = [exists e] then
                exists_e(rule,facts,true) -> (rule,flag,list);
            endif;
            if rule = [] or rule = [open box] then
            else
                [^^rulesused ^rule] -> rulesused;
            endif;
        endunless;
        unless flag == true then
            false -> flag2;
            npr('Please type in the next formula');
            readline() -> newformula;
            if newformula = [bye] then
                true -> topflag;
                quitloop();
            endif;
            unless rule = [var] do
                parse_formula( remove_commas(newformula),lang)-> formula;
                if isstring(formula) then
                    until not(isstring(formula)) do
                        npr(formula);
                        npr('Please try again');
                        readline() -> newformula;
                        if newformula = [bye] then
                            true -> topflag;
                            quitloop();
                        endif;
                        parse_formula( remove_commas(newformula),lang) -> formula;
                    enduntil;
                endif;
            endunless;
            if rule = [/\ e] then
                check_and_e(formula,list,rulesused) ->(formula,flag2,rulesused);
            elseif rule = [/\ i] then
                check_and_i(formula,facts,rulesused) ->(formula,flag2,rulesused);
            elseif rule = [\/ i] then
                check_or_i(formula,facts,rulesused) ->(formula,flag2,rulesused);
            elseif rule = [\/ e] then
                check_or_e(formula,rulesused,concls) ->(formula,flag2,rulesused);
            elseif rule = [-> i] then
                check_implies_i(formula,facts,rulesused) ->(formula,flag2,rulesused);
            elseif rule = [-> e] then
                check_implies_e(formula,facts,rulesused) ->(formula,flag2,rulesused);
            elseif rule = [~ i] then
                check_not_i(formula,facts,rulesused) ->(formula,flag2,rulesused);
            elseif rule = [~ e] then
                check_not_e(formula,facts,rulesused) ->(formula,flag2,rulesused);
            elseif rule = [~~] then
                check_notnot(formula,facts,rulesused) ->(formula,flag2,rulesused);
            elseif rule = [carry] then
                check_carry(formula,facts,rulesused) ->(formula,flag2,rulesused);
            elseif rule = [= i] then
                check_equals_i(formula,rulesused) ->(formula,flag2,rulesused);
            elseif rule = [= e] then
                check_equals_e(formula,formulas,equalterms,rulesused) -> (formula,flag2,rulesused);
            elseif rule = [var] then
                check_var_rule(newformula,facts,rulesused) -> (formula,flag2,rulesused);
            elseif rule = [all i] then
                check_all_i(formula,list,rulesused) ->(formula,flag2,rulesused);
            elseif rule = [all e] then
                check_all_e(formula,list,rulesused) ->(formula,flag2,rulesused);
            elseif rule = [exists i] then
                check_exists_i(formula,list,rulesused) ->(formula,flag2,rulesused);
            elseif rule = [exists e] then
                check_exists_e(formula,list,rulesused) ->(formula,flag2,rulesused);
            endif;
            if formula = [] or topflag then
            else
                [^^formulae ^formula] -> formulae;
                [^^facts ^formula] -> facts;
                [^^newfacts ^formula] -> newfacts;
                if formula = conc and boxes = 0 then
                    proofbox(formulae,rulesused,true,conc);nl(1);
                    npr('Well done, you have successfully derived the conclusion');
                    true -> topflag;
                else
                    proofbox(formulae,rulesused,false,conc);nl(1);
                endif;
            endif;
            newfacts -> proof;
        endunless;
    enduntil;
    if rule = [close box] and boxes > 0 do
        [^^formulae ^rule] -> formulae;
        boxes - 1 -> boxes;
        proofbox(formulae,rulesused,false,conc); nl(1);
    endif;
enddefine;

define get_conc(lang) -> conc;
    lvars conc, lang;
    npr('Please type in what formula you are trying to conclude');
    readline() -> conc;
    parse_formula( remove_commas(conc),lang)-> conc;
    until not(isstring(conc)) do
        npr(conc);
        npr('Please try again');
        readline() -> conc;
        parse_formula( remove_commas(conc),lang) -> conc;
    enduntil;
enddefine;

define print_lang(lang);
    lvars lang;
    vars item;
    npr('The following are predicates:'); nl(1);
    if hd(lang) = [] then
        tabs(1);npr('NO PREDICATES');nl(1);
    else
    for item in hd(lang) do
        tabs(1);pr(front(item)); pr(' of arity '); npr(back(item));
    endfor;nl(1);
    endif;
    npr('The following are functions:');nl(1);
    if last(lang) = [] then
        tabs(1);npr('NO FUNCTIONS');nl(1);
    else
    for item in last(lang) do
        tabs(1);pr(front(item)); pr(' of arity '); npr(back(item));
    endfor;
    nl(1);
    endif;
enddefine;

define get_lang(lang) -> lang;
    lvars lang, predicate, func, boole=false;
    vars item, name, var;
    npr('When you have finished defining the predicates please type no');
    npr('Please type in the predicate in the form name/arity');
    repeat
        nl(1);
        npr('Please type in the new predicate');
        readline() -> predicate;
    quitif(predicate = [no]);
        if predicate matches [?name / ?var:isinteger] then
            for item in hd(lang) do
                if name = front(item) then
                    true -> boole;
                    quitloop();
                else
                    false -> boole;
                endif;
            endfor;
            if member(name,quantifiers) or member(name,connectwds) then
                npr('The predicate name you have typed in is a special word');
            elseif boole = true then
                npr('The predicate name you have typed in is already in the language');
            else
                [[^^(hd(lang)) %conspair(hd(predicate),last(predicate))%] ^(last(lang))] -> lang;
            endif;
        else
            npr('You did not type in the predicate in the form name/arity');
        endif;
    endrepeat;
    edit(vedlmr_print_in_file);
    ved_clear();
    npr('When you have finished defining the functions please type no');
    npr('Please type in the function in the form name/arity');
    repeat
        nl(1);
        npr('Please type in the new function');
        readline() -> func;
    quitif(func = [no]);
        if func matches [?name / ?var:isinteger] then
            for item in hd(lang) do
                if name = front(item) then
                    true -> boole;
                    quitloop();
                else
                    false -> boole;
                endif;
            endfor;
            for item in last(lang) do
                if name = front(item) then
                    true -> boole;
                    quitloop();
                else
                    false -> boole;
                endif;
            endfor;
            if member(name,quantifiers) or member(name,connectwds) then
                npr('The function name you have typed in is a special word');
            elseif boole = true then
                npr('The function name you have typed in is already in the language');
            else
                [^(hd(lang)) [^^(last(lang)) %conspair(hd(func),last(func))%]] -> lang;
            endif;
        else
            npr('You did not type in the function in the form name/arity');
        endif;
    endrepeat;
    edit(vedlmr_print_in_file);
    ved_clear();
    npr('You have defined the following language');nl(1);
    print_lang(lang);
enddefine;

define get_new_lang(lang,flag)-> new_lang;
    lvars lang, new_lang, option, flag, num2 = 2, num3 = 3;
    vars check_lang;
    if flag then
    else
        edit(vedlmr_print_in_file);
        ved_clear();
        npr('The current language is defined below');nl(1);
        print_lang(lang);
    endif;
    npr('Select one of the following by typing in the number and then pressing return');
    nl(1);
    if flag = false then
        tabs(1);npr('1: Keep the old language');
    else
        num2 -> num3;
        1 -> num2;
    endif;
    tabs(1);pr(num2);npr(': Add to the old language');
    tabs(1);pr(num3);npr(': Create a new language');
    readline() -> option;
    until member(option,[[1] [^num2] [^num3]]) do
        npr('Please type in the number corresponding to the option you want');
        npr('and then press return');
        readline() -> option;
    enduntil;
    if flag then
        [^(hd(option) + 1)] -> option
    endif;
    if option = [1] then
        lang -> new_lang;
    elseif option = [2] then
        edit(vedlmr_print_in_file);
        ved_clear();
        get_lang(lang) -> new_lang;
        check_lang(new_lang) -> new_lang;
    elseif option = [3] then
        edit(vedlmr_print_in_file);
        ved_clear();
        get_lang([[][]]) -> new_lang;
        check_lang(new_lang) -> new_lang;
    endif;
enddefine;

define check_lang(lang) -> new_lang;
    lvars lang, new_lang, ans;
    npr('Do you wish to change the language?');
    readline() -> ans;
        until ans = [yes] or ans = [no] do
            npr('Please type in yes or no');
            readline()-> ans;
        enduntil;
    if ans = [no] then
        lang -> new_lang;
    else
        nl(1);
        get_new_lang(lang,true) -> new_lang;
    endif;
enddefine;

define deduction();
    lvars proof, conc, ans, formulae,rulesused,boxes,topflag;
    lvars funcs, preds;
    vars lang;
    edit(vedlmr_print_in_file);
    vedsetwindow();
    ved_clear();
    get_lang([[][]]) -> lang;
    check_lang(lang) -> lang;
    get_conc(lang) -> conc;
    edit(vedlmr_print_in_file);
    ved_clear();
    interface([],[], false, false,false,0,[],[],conc,lang) -> (proof,formulae,rulesused,boxes,topflag);
    repeat
        npr('Do you want to do another proof?');
        readline()-> ans;
        until ans = [yes] or ans = [no] do
            npr('Please type in yes or no');
            readline()-> ans;
        enduntil;
        if ans = [yes] then
            get_new_lang(lang,false)-> lang;
            get_conc(lang) -> conc;
            edit(vedlmr_print_in_file);
            ved_clear();
            interface([],[], false, false,false,0,[],[],conc,lang) -> (proof,formulae,rulesused,boxes,topflag);
        else
            npr('Goodbye');
            return();
        endif;
    endrepeat;
enddefine;
