Implementation of FeatherweightGo in makam [WIP]

fg.makam

% makam Antonis Stampoulis
% Tweag, PL nuevo
% makam me permitia experimentar rapido

% makam es:
% .. un dialecto de lambda prolog
% .. un lenguaje con muchas construcciones de reflexion

father : string -> string -> prop.

father "juan" "pedro".
father "juan" "melisa".
father "tomas" "juan".
father "anakin" "luke".

brother : string -> string -> prop.

brother A B :-
  father X A,
  father X B,
  not (eq A B).

grandpa : string -> string -> prop.

grandpa A B :-
  father A X,
  father X B.


% https://arxiv.org/pdf/2005.11710.pdf

% Fig 9
% -----
% FG syntax

% field = string.
% method = string.
% variable ???
% ts, ti, t = string.


expr : type.

method_sig : type.

method_sig : list string -> string -> method_sig.

method_spec : type.
method_spec : string -> method_sig -> method_spec.

type_lit : type.

struct : list (tuple string string) -> type_lit.
interface : list method_spec -> type_lit.

decl : type.

type_decl : string -> type_lit -> decl.
method_decl : string -> method_spec -> (expr -> bindmany expr expr) -> decl.

% func (x ts) m (x1 t1, x2 t2, ... )t {return e}
% \x. \x1 x2 ... xn. e

program : type.
program : list decl -> expr -> program.

method_call : expr -> string -> list expr -> expr.
struct_lit : string -> list expr -> expr.
select : expr -> string -> expr.
type_ass : expr -> string -> expr.


% Fig 10
% ------
% auxiliary functions

global_decl : list decl -> prop.

fields : string -> list (tuple string string) -> prop.

fields TS L :-
  global_decl D,
  contains (type_decl TS (struct L)) D.

body : string -> string -> (expr -> bindmany expr expr) -> prop.

body TS M F :-
  global_decl D,
  contains (method_decl TS (method_spec M _) F) D.

type_aux : expr -> string -> prop.
type_aux (struct_lit TS _) TS.

unique : list method_spec -> prop.

unique [].
unique ((method_spec Name Sig) :: TL) :-
  unique TL,
  if (contains (method_spec Name Sig') TL)
  then eq Sig Sig'
  else success. 


% doc: https://github.com/astampoulis/makam/blob/master/stdlib/list.makam

tdecls : list decl -> list string -> prop.
tdecls_aux : decl -> string -> prop.

tdecls D TS :-
  map tdecls_aux D TS.

tdecls_aux (type_decl S _) S.

mdecls : list decl -> list (tuple string string) -> prop.
mdecls_aux : decl -> (tuple string string) -> prop.

mdecls D TS :-
  map mdecls_aux D TS.

mdecls_aux (method_decl S (method_spec S2 _) _) (S, S2).

methods_s : string -> list method_spec -> prop.
methods_aux : string -> decl -> prop.
methods_aux2 : decl -> method_spec -> prop.

methods_s TS MS :-
  global_decl D,
  filter (methods_aux TS) D D',
  map (methods_aux2) D' MS.


methods_aux TS (method_decl TS _ _).
methods_aux2 (method_decl _ M _) M.

methods_i : string -> list method_spec -> prop.
methods_i TI MS :-
  global_decl D,
  contains (type_decl TI (interface MS)) D.



% \/ Borrador 
% methods_i TI MS :-
%  gdecl (type_decl TI (interface MS)).

%  filtermap : (A -> B -> prop) -> list A -> list B -> prop.


global_decl [
  type_decl "coord" (struct [("x", "int"), ("y", "int")]),
  method_decl "coord" (method_spec "combine" (method_sig ["coord"] "coord"))
    (fun this => bind _ (fun other => (body
      (type_ass (struct_lit "coord" [
          select this "x",
          select other "y"
      ]) "coord")
    )))
    % :: (expr -> bindmany expr expr)
    % bind : string -> (A -> bindmany A B) -> bindmany A B.
    % body : B -> bindmany A B.

].

% A -> A -> .... -> A -> B
% bindmany.

fields "coord" L ?

% (
%     gdecl (
%         type_decl "coord" (struct [("x", "int"), ("y", "int")])
%     ) -> 
%     (gdecl (....) -> fields "coord" L, print "foo")
% )?


% data AST = ... | Function (AST -> AST) | ...

% typecheck :: AST -> type -> bool
% typecheck (Function f) (Arrow a b) = 
%   (x : AST -> typecheck x a -> typecheck (f x) b)

% rlwrap

% gdecl : decl -> prop.