module collp.

% lambda prolog - col translation

% col type judgements:

% the translation:  (into beta-eta long normal form for now)

tau cint (cic N) N L :- not (compound N).
tau cstring (csc S) S L :- not (compound S).
tau creal (crc R) R L :- not (compound R).
tau clist cnil [] L.
tau clist (ccons A B) [C|D] L :- tau T A C L, tau T B D L.

% generic clauses to be augmented by signature-specific clauses generated
% by meta-compiler for each COL signature.
% uncomment to trace:
%tau A B C D :- printterm std_out (tau A B C D), print " <--\n", fail.

% critical clauses for abstraction:  (negative)

% correct way:
tau (cr (cr cint cint) cint) (cabs A) B L :-  !, L1 is (L + 1),
  pi v\ ( (pi N\ (pi M\ (pi C\ (pi D\ (
	     tau cint (capp (ind N) C) (v D) M :-
			N is (M - L), tau cint C D M)))))
	  => (tau cint A (B v) L1)).

% generic third order constants
tau (cr (cr S1 S2) T) (cabs A) B L :- not (S1 = (cr S11 S12)), L1 is (L + 1),
  pi v\ ( (pi N\ (pi M\ (pi C\ (pi D\ (
	     tau S2 (capp (ind N) C) (v D) M :-
			N is (M - L), tau S1 C D M)))))
	  => (tau T A (B v) L1)).

tau (cr S T) (cabs A) B L :-  not (S = (cr S1 S2)), L1 is (L + 1), 
  pi v\ ( (pi N\ (pi M\ (tau S (ind M) v N :- M is (N - L))))
		=> (tau T A (B v) L1)).

tau (cr S T) (cabs A) B L :-  L1 is (L + 1), 
  pi v\ ( (pi N\ (pi M\ (tau S (ind M) v N :- M is (N - L))))
		=> (tau T A (B v) L1)).


type primtype ctype -> o.
primtype cint.
primtype creal.
primtype clist.
primtype cstring.
primtype (tid N).



% client-server setup:

open_col_session Hostaddr (scsession In Out) :-
  open_socket Hostaddr 20027 In Out.   % 20027 is COLP port
close_col_session (scsession In Out) :-
%  output Out "$",
  close_in In, close_out Out.

remote_eval (scsession In Out) S T :-
  tau COLTYPE CS S 0,   % CS is COL representation of meta-level S.
  % translate CS into string form - CSSTRING
     term_to_string CS CS2,   % temporary, will use prettyprint function.
  output Out CS2, flush Out,   % send COL term to server
  read_carefully In Response,
  % translate string to a COL term - temporary solution:
  %print Response, print "  --  \n",
     string_to_term Response Answer,
  tau COLTYPE Answer T 0.  % type and translate to meta-level term.

type read_carefully in_stream -> string -> o.    
read_carefully In S :- input In 1 G, 
  ((G = "$", S = "");  
   (read_carefully In T, S is (G ^ T))), !.


%   special for scheme server

callC A B C :- remote_eval A B C.

callscheme (scsession In Out) S T :-
  tau Ctype CS S 0,
  term_to_string CS CS1,
  CS2 is ("(" ^ CS1 ^ ")"),
%print CS2, print "   ..\n",
  output Out CS2, flush Out,
  read_carefully In Response,
  string_to_term Response Answer,
  tau Ctype Answer T 0.