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.