module toplevel.

tl ActiveGoals Counter ((input Gname Tac)::Is) :-
  gstore Gname Goal, Tac Goal NewGoal,
  memb_and_rest Gname ActiveGoals NewAG,
  tl NewAG Counter ((spawn NewGoal)::Is).

tl ActiveGoals Counter ((spawn tt)::Is) :-
  read_command Command, tl ActiveGoals Counter Is.

tl ActiveGoals Counter ((spawn (G cc H))::Is) :-
  tl ActiveGoals Counter (spawn G::spawn H::Is).

tl ActiveGoals Counter ((spawn (all G))::Is) :-
  pi x\ tl ActiveGoals Counter (spawn (G x)::Is).

tl ActiveGoals Counter ((spawn (Vs | Gamma --> G))::Is) :-
  pi x\ gname Counter (Vs | Gamma --> G) =>
        (Counter' is (Counter + 1),
         tl (Counter::ActiveGoals) Counter' Is).