module defs.

import lists, control, maps.
import goals, tacticals.
import fol, folpn, lj, parser, printer.
import subst, unify.

type backchain    form -> form -> form -> o.

backchain (forall _ B) A G     :- !, backchain (B T) A G.
backchain (G imp A)    A G     :- !.
backchain A            A truth :- atomic A.

kind nameD        type.
type default_def  list form -> o.

type defr      int -> goal -> goal -> o.

defr N (Vs | Delta --> A) (Vs | Delta --> NewG) :-
  default_def Defs,
  nth_item N Def Defs,
  load_pnames Vs (backchain Def A NewG).

type defl      int  -> goal -> goal -> o.
type defl'     form  -> form -> goal -> goal -> o.

defl N (Vs | Delta --> B) Gs :-
  nth_and_rest N A Delta Delta',
  atomic A, 
  default_def Defs,
  mappred (x\y\ defl' x A (Vs | Delta' --> B) y) Defs Glist,
  conj_goal Glist Gs.

defl' (forall Str D) A (Vs | Delta --> B) (all G) :- !,
 pi v\ defl' (D v) A ((pr v Str)::Vs | Delta --> B) (G v).

defl' (Body imp Head) A (Vs | Delta --> B) G :- !,
  load_vars Vs 
    (if (unify Head A Mgu)
        (apply_sub B Mgu B',
         mappred (c\d\ apply_sub c Mgu d) (Body::Delta) Delta',
         G = (Vs | Delta' --> B'))
        (G = tt)).

defl' Head A (Vs | Delta --> B) G :-
  atomic Head, 
  load_vars Vs 
   (if (unify Head A Mgu)
       (apply_sub B Mgu B',
        mappred (c\d\ apply_sub c Mgu d) Delta Delta',
        G = (Vs | Delta' --> B'))
       (G = tt)).