:-op(200,xfx,'::').
:-op(800,fx,'$').
:-use_module(library(lists)).
:-multifile '::'/2.

% rtcheck(+Rprev, +Rrest, ?RT)
%
% Typechecker for records. RT is the record type of the record Rrest, possibly
% including types dependent on Rprev, the part of the record which has already
% been checked. Typically called with Rprev=[]. If RT is a variable, it will be 
% instantiated with the record type corresponding to Rrest which has the same 
% number of fields as Rrest.

% case 1: base case.

rtcheck(_,[],[]).

% case 2, dependent type.

rtcheck(Rprev,[L=V|Rrest],[L::Fun|RTrest]):-
	\+ var(Fun),
	Fun =.. [Function|Args],         
	\+ Args = [],                    % if it has arguments, it's a function.
	subst(Rprev, Args, NewArgs),     % substitute values for paths
	append([Function|NewArgs],[T],PredList), % make function into predicate
	Pred =.. PredList,                    
	Pred,                            % call predicate, returning type
	V::T,                            
	append(Rprev,[L=V],NewRprev),    % add checked field to Rprev
	rtcheck(NewRprev,Rrest,RTrest).


%| ?- [a=true,b=true]::[a::bool, b::f(type,a)].
%
%yes

% case 2, non-dependent type

rtcheck(Rprev,[L=V|R],[L::T|RT]):-
	V::T,
	append(Rprev,[L=V],NewRprev),
	rtcheck(NewRprev,R,RT).


% case 3: subsumption.

rtcheck(Rprev,[L=V|R],[M=W|RT]):-
	\+ L=M,
	V::_,
	append(Rprev,[L=V],NewRprev),
	rtcheck(NewRprev,R,[M=W|RT]).


% +Record::+RecordType
%
% Type checking for simple types and record types.
% These are special cases. The main part of the simple type declarations
% are situation-dependent.

% Type checking for record types is a special case

R::RT:-is_list(R),rtcheck([],R,RT).






% value(+Record, +Path, -Value)
%
% Value is the value of Path in Record

value([L=V|_],L,V):-!.
value([L1=R1|_],L1*L,V):-
	value(R1,L,V).
value([_|R],P,V):-
	value(R,P,V).


% subst(+Record, +ArgList, - NewArgList)
%
% NewArgList is ArgList with all paths replaced by the corresponding value in 
% Record.

subst(_,[],[]).

subst(Record,[$Path|Args], [Value|NewArgs]):-
	value(Record, Path, Value),
	subst(Record, Args, NewArgs).

subst(Record, [RecordArg|Args], [NewRecordArg|NewArgs]):-
	is_list(RecordArg),!,                              % Arg is a record
	subst_record(Record, RecordArg, NewRecordArg),
	subst(Record, Args, NewArgs).

subst(Record,[Value|Args],[Value|NewArgs]):-
	subst(Record, Args, NewArgs).


% subst_record(+Record, +RecordArg, -NewRecordArg)
%
% NewRecordArg is RecordArg with all paths replaced by the corresponding value in 
% Record.

subst_record(_, [], []).

subst_record(Record, [Label=Arg|Args], [Label=NewArg|NewArgs]):-
	subst(Record, [Arg], [NewArg]),
	subst_record(Record, Args, NewArgs).




% type(+Record, +Path, -Type)
%
% Type is the type of the value of Path in Record

type0(Value, Type):-
	Value::Type.






%
% Some situation theoretical notions
%



% (inhabited) propositions are types of proofs

prf(Prop)::Prop :- Prop.
%[prf(Prop1),prf(Prop2)]::and(Prop1,Prop2) :- Prop1, Prop2.


% Basic infon type

X::infon :- X::[rel::rel, args::appr($rel), pol::bool].


% appr0(+Rel, -Args)
% 
% Args is the appropriate arguments for relation Rel.

% (defined externally)
% Example: 
% appr(hire,[hirer::ind, hired::ind]).

/*
appr0(Rel,Args):-
	Rel::rel,
	appr(Rel, Args).
*/

/*
| ?- [rel=hire, args=[hirer=ind56, hired=ind57], pol=1]::[rel::rel, args::appr($rel),pol::bool].

yes
*/

% classify0(+Infon, +Sit, -Prop)
%
% This is the a predicate implementing the function corresponding to 
% the two-place "classify" relation. This is a consequence of seeing all values
% which take arguments as functions. 

classify(Infon, Sit, classify(Infon, Sit)).

/*
classify0(Infon, Sit, classify(Infon, Sit)):-
	Infon::infon.
*/

/*
| ?- [ref0=ind56, sit0=sit5001, prf0=proof10]::[ref0::ind,sit0::sit,prf0::classify([rel=named,args=[named=$ref0,name='Smith'],pol=1], $sit0)].

yes

| ?- [ref0=ind56, sit0=sit5001, prf0=prf(classify([rel=named,args=[named=ind56,name='Smith'],pol=1],sit5001))]::[ref0::ind,sit0::sit,prf0::classify([rel=named,args=[named=($ref0),name='Smith'],pol=1], $sit0)].

yes
*/




/*

[a=1,b=0]::[a::int,b:: R::[a::int]^T(R.a)], T is a function; in none, then identity (same type as the value, i.e. same type as for the path)

% simple path

[a=1,b=0]::[a::int, b:: R::[a::int]#R*a]
[a=1,b=0]::[a::int, b::type(a)]

[a=1,b=0,c=1]::[a::int, b:: R1::[a::int]^T(R1.a), 
	c:: R::[a::int, b:: R1::[a::int]^T(R1.a)]^T(R.a, R.b)


generally:

... :: [L1::T1,
	L2::(R1::[L1::T1](T2(R1.L1))),
	L3::(R2::[L1::T1,
	          L2::(R1::[L1::T1](T2(R1.L1)))
		 ](T3(R1.L1, R2.L2))),
	...]

Abbreviated:

... :: [L1::T1,
	L2::T2(L1),
	L3::T3(L1,L2),
	...]


APPR function

[rel=hire, args=[hirer=jones, hired=smith], pol=1]::[rel::relT, args::(R::[rel::relT](f(appr,R*rel))),pol:bool]

CLASSIFY is a _relation_, not a function

[ref0=ind56, sit0=sit5001, prf0=prf(classify(sit5001,[rel=named,args=[referent=ind56,name='Smith'],pol=1]))]::[ref0::ind,sit0::sit,prf0::classify(sit0,[rel=named,args=[referent=ref0,name='Smith'],pol=1])].

PRF function from proposition to proof

*/