module rules.

import lists.
import goals, tacticals.
import fol, aux, lj, parser, printer.

type initial                  int -> goal -> goal -> o.
type weaken                   int -> goal -> goal -> o.

initial N (Vs | Delta --> P) tt :- nth_item N P' Delta, eq_form P P', !.
weaken  N (Vs | Delta --> P) (Vs | Delta' --> P) :- 
   nth_and_replace N _ Delta nil Delta'.

% Right introduction rules.

type truth_r, and_r, or_r1, or_r2, imp_r, neg_r    goal -> goal -> o.

truth_r (Vs | Delta --> truth)     tt.
and_r   (Vs | Delta --> (A and B)) ((Vs | Delta --> A) cc (Vs | Delta --> B)).
or_r1   (Vs | Delta --> (A or  B)) (Vs | Delta --> A).
or_r2   (Vs | Delta --> (A or  B)) (Vs | Delta --> B).
imp_r   (Vs | Delta --> (A imp B)) (Vs | (A::Delta) --> B).
neg_r   (Vs | Delta --> (neg A))   (Vs | (A::Delta) --> false).

% Left introduction rules.

type and_l, imp_l, neg_l, or_l       int -> goal -> goal -> o.

and_l N (Vs | Delta --> C) (Vs | Delta' --> C) :-
   nth_and_replace N (A and B) Delta (A::B::nil) Delta'.

or_l  N (Vs | Delta --> C) ((Vs | Delta' --> C) cc (Vs | Delta'' --> C)) :-
   nth_and_replace N (A or  B) Delta (A::nil) Delta',
   nth_and_replace N (A or  B) Delta (B::nil) Delta''.

imp_l N (Vs | Delta --> C) ((Vs | Delta --> A) cc (Vs | Delta' --> C)) :-
   nth_and_replace N (A imp B) Delta (B::nil) Delta'.

neg_l N (Vs | Delta --> C) (Vs | Delta --> A) :- 
   nth_item N (neg A) Delta.

% Quantifier rules

type forall_r                    goal -> goal -> o.
type exists_r          string -> goal -> goal -> o.
type exists_l             int -> goal -> goal -> o.
type forall_l   string -> int -> goal -> goal -> o.
type forallk_l  string -> int -> goal -> goal -> o.

forall_r     (Vs | Delta --> (forall Name B))
             (all y\(((pr y Name)::Vs) | Delta --> (B y))).

exists_r Str (Vs | Delta --> B) (Vs | Delta --> Instan) :-
  load_pnames Vs (read_terms Str Ts),
  instan_exists B Ts Instan.

forall_l Str N (Vs | Delta --> C) (Vs | Delta' --> C) :-
  nth_and_replace N B Delta (Instan::nil) Delta',
  load_pnames Vs (read_terms Str Ts),
  instan_forall B Ts Instan.

forallk_l Str N (Vs | Delta --> C) ((Vs | ((B T)::Delta)) --> C) :-
  nth_item N (forall _ B) Delta,
  load_pnames Vs (read_term Str T).

exists_l N   (Vs | Delta --> C) 
             (all y\ (((pr y Name)::Vs) | (Delta' y) --> C)) :-
   pi y\(nth_and_replace N (exists Name B) Delta ((B y)::nil) (Delta' y)).

% Query for quantifiers instances.

type query_term   list (pair i string) -> i -> o.

query_term Vars Term :- 
  handle _
   (print "Enter term: ", 
    input_line std_in Str, 
    load_pnames Vars (read_term_line Str Term))
   (print "Error.  Re",  query_term Vars Term).

type forallq_l        int -> goal -> goal -> o.
type existsq_r               goal -> goal -> o.

existsq_r    (Vars | Delta --> (exists _ B))
             (Vars | Delta --> (B T)) :- 
   query_term Vars T.

forallq_l N  (Vars | Delta --> C)
             ((Vars | ((B T)::Delta)) --> C) :-
   nth_item N (forall Name B) Delta, !, query_term Vars T.


% Convert a pre-tactical into a tactical.

local in_range      int -> int -> int -> o.

in_range _ N M :- M < N, !, fail.
in_range N N M.
in_range I N M :- N' is N + 1, in_range I N' M.

type pre     (int -> goal -> goal -> o) -> goal -> goal -> o.

pre PreTac (Vars | Delta --> B) Out :-
  length Delta L, in_range N 1 L, PreTac N (Vars | Delta --> B) Out.

% A simple automatic tactic.

type go           goal -> goal -> o.

go In Out :- 
  repeat 
   (orelse (pre initial)
   (orelse truth_r
   (orelse imp_r    
   (orelse neg_r
   (orelse forall_r
   (orelse (pre and_l)
   (orelse (pre exists_l)
   (orelse and_r (pre or_l)))))))))
   In Out.