% From Prolog to λProlog
% λProlog adds some extensions to normal Prolog:
% - polymorphic typing
% - higher-order programming
% - hypothetical reasoning
%
% That makes the logic corresponding to λProlog that of higher-order hereditary harrop formulae.

%% Polymorphic Typing:
kind person type.

type sokrates person.
type plato person.
type zeno person.
type aristotle person.

pred mentor o:person o:person.
% this is roughly equivalent to
% `type mentor person -> person -> o.`
% where `o` is the type of propositions

mentor sokrates plato.
mentor plato aristotle.

pred influenced o:person o:person.
influenced X Y :-
    mentor X Y.

influenced X Y :-
    mentor X Z,
    influenced Z Y.

pred age o:person o:int.

age sokrates 70.
age plato 23.
age zeno 90.

pred older o:person o:person.
older X Y :-
  age X N,
  age Y M,
  N > M.

kind node type.
pred adj o:node o:node.
pred path o:node o:node.

path X Y :-
  adj X Z,
  path Z Y.

% Type constructors are also allowed:
kind mylist type -> type.

%% Higher-Order Programming:
%
% So far we've only seen a typed version of Prolog.
% λProlog adds another term constructor: lambda abstractions
% e.g.
%
% Id = x\ x

pred mentor-f i:(person -> person) o:person.
mentor-f F X :-
  mentor (F X) X.

pred map o:(A -> B) o:list A o:list B.
map _F nil nil.
map F (X :: L) ((F X) :: L1) :-
  map F L L1.

pred fold o:(A -> B -> B) o:list A o:B o:B.
fold _F nil B B.
fold F (X :: L) B (F X R) :-
  fold F L B R.

%% Hypothetical Reasoning
% λProlog allows scoped assumptions
%
% `rule => body` adds `rule` to the top of the program, then runs `body`.
% once `body` terminates `rule` is removed from the context

% Concrete Syntax:
kind lam type.
type lam-abs string -> lam -> lam.
type lam-app lam -> lam -> lam.
type lam-var string -> lam.

% de Bruijn:
kind db type.
type db-var int -> db.
type db-abs db -> db.
type db-app db -> db -> db.

pred depth o:int o:string.

pred lam->db o:lam i:int o:db.
lam->db (lam-app L R) D (db-app L1 R1) :-
  lam->db L D L1,
  lam->db R D R1.

lam->db (lam-abs V B) D (db-abs B1) :-
  D1 is D + 1,
  depth D V => lam->db B D1 B1.

lam->db (lam-var V) D (db-var I) :-
  depth N V,
  I is D - N - 1.

%% Scoped Quantification
% λProlog adds the term constructors `pi` and `sigma`, for universal/existential quantification.
% They are implemented as higher-order term constructors:
%
% pi x\ mentor sokrates x
%
% sigma y\ mentor y plato

pred all i:(A -> o) i:list A.
all _P nil.
all P (X :: L) :-
  P X,
  all P L.

pred some i:(A -> o) i:list A.
some P (X :: _L) :- P X.
some P (_X :: L) :- some P L.

%%% Explicit Quantification:

% All of the following are equivalent:
path X Y :- adj X Z, path Z Y.

path X Y :- sigma z\ adj X z, path z Y.

pi x\ pi y\
   (path x y :-
         sigma z\ adj x z, path z y).

%%% HOAS

kind tm, ty type.
type app tm -> tm -> tm.

% A lambda abstraction is just a function:
type abs (tm -> tm) -> tm.

type arrow ty -> ty -> ty.


% The typing rules showcase higher-order unification:
pred of i:tm o:ty.
of (app M N) T :-
  of M (arrow U T),
  of N U.

of (abs R) (arrow T U) :-
  pi x\ of x T => of (R x) U.