pa.elpi

% TODO:
% - modificare eq per poter prendere in input il nome di un termine e poter
%   elaborare ulteriormente il termine tramite unificazione

accumulate itt/theory.
accumulate itp.

loop_end S :- print S.
%loop_aux A B :- print (loop_aux A B), fail.
loop_aux D S :-
    print D, print_constraints, print,
    read T, (T = quit, loop_end S, !;
    process_input T D D' PS, append S [T, PS] S', loop_aux D' S').
start :- loop_aux (pa_state [] []) [].

mode (process_input i i o o).
%process_input A B C D :- print (process_input A B C D), fail.

% arbitrary type introduction
process_input (axiom N T) (pa_state D NG) (pa_state D' NG) [] :-
    append D [conv N T, conv T N] D',
    pa_print (axiom N T).

% full definition, check convertibility
process_input (define N ty T te X) (pa_state D G) (pa_state D' G') [] :-
    D => (of X S X', conv S T),
    build_newgoals X' [] NG,
    append NG G G',
    append D [of N T X', step N X] D',
    pa_print (define N ty T te X).

% only X, infer T
process_input (define N te X) (pa_state D G) (pa_state D' G') [] :-
    D => of X T X',
    build_newgoals X' [] NG,
    append NG G G',
    append D [of N T X', step N X] D',
    pa_print (define N ty T te X').

% only T, enter proof mode
process_input (define N ty T) (pa_state D G) (pa_state D' G') PS :- 
    D => (of X T X', prove X T X' PS),
    build_newgoals X' [] NG,
    append NG G G',
    append D [of N T X', step N X] D',
    pa_print (define N ty T te X').

% unification i.e. assert that two terms are equal
process_input (eq T T') (pa_state D G) (pa_state D G') [] :-
    check_conv D T T',
    build_newgoals T' [] NG,
    append NG G G',
    pa_print (eq T T').
    
check_conv As T T' :-
    As => (of T A _, of T' B _, conv A B, conv T T').

process_input start_proof_mode (pa_state D G) (pa_state D G') PS :-
    D => prove G G' PS.

pa_print (axiom N T) :-
    term_to_string N NS, pp T ST, S is NS ^ ": " ^ ST, print S.
pa_print (define N ty T te X) :-
    term_to_string N NS, pp T ST, pp X SX, S is NS ^ ": " ^ ST ^ " ≅ " ^ SX, print S.
pa_print (eq T T') :-
    pp T ST, pp T' ST', S is ST ^ " ≡ " ^ ST', print S.