module goals.

kind    goal            type.

type    tt, ff          goal.
type    cc, vv          goal -> goal -> goal.
type    allg            (A -> goal) -> goal.

infixl  vv              3.
infixl  cc              3.

type    maptac  (goal -> goal -> o) -> goal -> goal -> o.

maptac Tac tt         tt         :- !.
maptac Tac (I1 cc I2) (O1 cc O2) :- !, maptac Tac I1 O1, maptac Tac I2 O2.
maptac Tac (I1 vv I2) O          :- !, maptac Tac I1 O; maptac Tac I2 O.
maptac Tac (allg In)   (allg O)  :- !, pi t\ maptac Tac (In t) (O t).
maptac Tac In         O          :- Tac In O.

type goalreduce, red1, redex     goal -> goal -> o.

redex (tt cc Goal) Goal.
redex (Goal cc tt) Goal.
redex (allg T\tt) tt.

red1 G H :- redex G H, !.

red1 (G cc H) (Gx cc H) &
red1 (H cc G) (H cc Gx) &
red1 (G vv H) (Gx vv H) &
red1 (H vv G) (H vv Gx) :- red1 G Gx.

red1 (allg G)  (allg Gx)  :- pi x\ red1 (G x) (Gx x).

goalreduce G H :- red1 G Gx, !, goalreduce Gx H.
goalreduce G G.

type conj_goal   list goal -> goal -> o.

conj_goal nil tt.
conj_goal (G ::nil) G       :- !.
conj_goal (tt::Gs)  O       :- !, conj_goal Gs O.
conj_goal (G:: Gs) (G cc O) :-    conj_goal Gs O.