module top.

import goals, toploop, tacticals.   % Generic tactical stuff.
import control, lists.
import fol, folpn, lj, parser.      % Basic intuitionistic logic
import displays.                    % Various printing predicates
import rules, defs, formulas.       % Used for LJ theorem proving.
import nats, induction.             % For induction.
import defexs.                      % For definitions.

type display_names    o.
type prover           o.
type prove            nameT -> goal -> o.

display_names :-
  formula Name _, term_to_string Name Str, print Str, print " ", fail.
display_names.

prover :-
  print "The following formulas are available for proving:\n",
  display_names, print "\nEnter a formula name: ",
  read Name, prove Name _.

prove Name Out :- 
  formula Name Dec,
  load_dec Dec (F\ tl_loop (nil | nil --> F) Out).

type acc_defs    list nameD -> (list form -> o) -> o.

acc_defs nil G :- G nil.
acc_defs (D::Ds) G :-
  defex D _ Dec,
  load_decs Dec (L\ acc_defs Ds (K\ sigma M\ append L K M, G M)).

type dprover      nameT -> list nameD -> o.
type dp           nameT -> list form  -> o.

dprover Thm Defs :- acc_defs Defs (dp Thm).

dp Thm Ds :-
  formula Thm Dec,
  print "Definitions are:\n-----------------------------------\n",
  ((pi X\ ooo X :- output std_out X) => write_hyps 1 Ds),
  default_def Ds => load_dec Dec (F\ tl_loop (nil | nil --> F) _).