% The data type for intuitionistic sequents along with the code for 
% printing them.

module lj.

import lists, alist, maps, control.
import fol, folpn, goals, printer.

kind left       type.

type   |        list (pair i string) -> list form -> left.
type   -->      left -> form -> goal.
infix  |        4.
infix  -->      3.

type write_seq     goal -> o.
type write_vars    list (pair i string) -> o.
type write_hyps    int -> list form -> o.
type write_conc    form -> o.

write_seq (Vars | Delta --> C) :- 
  (pi X\ ooo X :- output std_out X) => 
  load_pnames Vars (write_vars Vars, write_hyps 1 Delta, write_conc C).

write_vars nil.
write_vars (V::Vs) :- 
  print "Vars: ",
  forevery
   (v\ (sigma N\sigma V\sigma H\ 
         (v = (pr V H), pname_term V N nil, print N, print " ")))
   (V::Vs),
  print "\n".

write_conc C           :- write_form C, print "\n".

write_hyps N nil       :- print "-----------------------------------\n".
write_hyps N (H::Hs)   :- 
  print "(", term_to_string N S, print S, print ") ", 
  write_form H, print "\n", M is (N + 1), write_hyps M Hs.