1% Copyright (C) Geoffrey Churchill 2023-2024
    2%
    3% This program is free software: you can redistribute it and/or modify
    4% it under the terms of the GNU General Public License as published by
    5% the Free Software Foundation, either version 3 of the License, or
    6% (at your option) any later version.
    7%
    8% This program is distributed in the hope that it will be useful, but
    9% WITHOUT ANY WARRANTY; without even the implied warranty of
   10% MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU
   11% General Public License for more details.
   12%
   13% You should have received a copy of the GNU General Public License
   14% along with this program. If not, see
   15% <https://www.gnu.org/licenses/>. 
   16
   17:- module(perfunctory_types, [
   18	      op(1150,  fx, type),
   19	      op(1130, xfx, --->),
   20	      op(1130,  fx, --->),
   21	      (type)/1,
   22	      typecheck/2,
   23	      retract_all_types/0
   24	  ]).   25
   26:- dynamic ctor_pretype_type/3. % Type definitions, e.g. ctor_pretype_type(s, s(nat), nat).
   27:- dynamic alias_canonical/2. % Type aliases, e.g. alias_canonical(intlist, list(int)).
   28
   29:- det((type)/1).   30
   31% Declare a new type. `PreTypes` should be a semicolon-delimited list of terms whose arguments are types.
   32type Type ---> PreTypes =>
   33    $(nonvar(Type)),
   34    $(nonvar(PreTypes)), % This ensures semicolon_list is det.
   35    $(allowed_functor(Type)),
   36    $(\+ declared_type(Type)), % Guardrail: single-definition.
   37    $(\+ declared_ctor(Type)), % Guardrail: types can't be ctors of other types.
   38    $(vars_preserved(PreTypes, Type)),
   39    $(semicolon_list(PreTypes, PreTypeList)),
   40    $(normalize(Type, NT)),
   41    maplist(assert_type(NT), PreTypeList).
   42
   43% If the derived type is omitted it will default to be the same as the ctor. This can be done in order to constrain a ctor's arity or argument types without needing to come up with a name for the derived type.
   44type ---> PreType => type PreType ---> PreType.
   45
   46% Declare `A` as an alias of `B`.
   47type A == B =>
   48    $(nonvar(A)),
   49    $(nonvar(B)),
   50    $(allowed_functor(A)),
   51    $(\+ declared_type(A)),
   52    $(\+ declared_ctor(A)),
   53    $(vars_preserved(B, A)), % This allows phantom types
   54    $(normalize(B, C)),
   55    $(assert_possibly_cyclic_alias_canonical(A, C)).
   56
   57normalize(A, C) :- cata(normalize_, A, C).
   58normalize_(A, C), A =@= (_ -> _) => C = A.
   59normalize_(A, C) => get_possibly_cyclic_alias_canonical(A, C) *-> true ; C = A.
   60
   61cata(F, A, B) :-
   62    copy_term(A, A_),
   63    rb_empty(Seen),
   64    cata_(F, Seen, A_, B),
   65    unescape(A_, A).
   66cata_(_, _,    A,  B), var(A) => A = please_evaluate_me_to(B).
   67cata_(_, _,   please_evaluate_me_to(B_), B) => B = B_.
   68cata_(F, Seen, A,  B) =>
   69    rb_insert_new(Seen, A, B, Seen1)
   70    -> same_functor(A, C), % Apply constraint early
   71       call(F, C, B),
   72       mapargs(cata_(F, Seen1), A, C)
   73    ;  rb_lookup(A, B, Seen). % Tie the knot
   74
   75unescape(A, B) :-
   76    rb_empty(Seen),
   77    cata_(id, Seen, A, B).
   78
   79id(A, A).
   80
   81assert_type(Type, PreType) :-
   82    $(allowed_functor(PreType)),
   83    $(\+ declared_ctor(PreType)), % If a ctor could appear in distinct type declarations it would require linear space and exponential time to find the right type.
   84    $(mapargs(normalize, PreType, NPT)), % Normalize arguments. This could just be normalize(PreType, NPT).
   85    $(functor(NPT, Ctor, _)),
   86    $(assert_possibly_cyclic_type(Ctor, NPT, Type)). % As of SWI 9.0.4, cyclic terms cannot be directly asserted.
   87
   88% See https://www.cs.cmu.edu/~fp/courses/lp/lectures/10-poly.pdf (type preservation).
   89vars_preserved(PreType, Type) :-
   90    term_vars_ord(PreType, PTVs),
   91    term_vars_ord(Type, TVs),
   92    ord_subset(PTVs, TVs).
   93
   94term_vars_ord --> term_variables, list_to_ord_set.
   95
   96skeletal(Term) :-
   97    Term =.. [_|Args],
   98    maplist(var, Args).
   99
  100allowed_functor(Term), nonvar(Term) =>
  101    Term \= (_ -> _), % (->)/2 is reserved for function types.
  102    Term \= please_evaluate_me_to(_). % (\)/1 is reserved for cata escapes.
  103
  104declared_type(Type) :-
  105    $(same_functor(Type, Skel)), % This allows arity-overloaded types. TODO Maybe should be disallowed as is done for ctors.
  106    (get_possibly_cyclic_type(_, _, Skel) ; alias_canonical(Skel, _)), !.
  107
  108declared_ctor(PreType) :-
  109    $(functor(PreType, Ctor, _)),
  110    ctor_pretype_type(Ctor, _, _).
  111
  112assert_possibly_cyclic_type(Ctor, PreType, Type) :-
  113    term_factorization(PreType, PTF),
  114    term_factorization(Type, TF),
  115    assertz(ctor_pretype_type(Ctor, PTF, TF)).
  116
  117get_possibly_cyclic_type(Ctor, PreType, Type) :-
  118    ctor_pretype_type(Ctor, PTF, TF),
  119    term_factorization(PreType, PTF),
  120    term_factorization(Type, TF).
  121
  122assert_possibly_cyclic_alias_canonical(A, C) :-
  123    term_factorization(C, Factorization),
  124    assertz(alias_canonical(A, Factorization)).
  125
  126get_possibly_cyclic_alias_canonical(A, C) :-
  127    alias_canonical(A, Factorization),
  128    term_factorization(C, Factorization).
  129
  130retract_all_types :-
  131    retractall(ctor_pretype_type(_, _, _)),
  132    retractall(alias_canonical(_, _)).
  133
  134term_factorization(Term, acyclic(Term_)) => Term = Term_.
  135term_factorization(Term, skel_subst(Skel, Subst)) =>
  136    Term = Skel,
  137    maplist(call, Subst).
  138term_factorization(Term, Factorization), var(Factorization) =>
  139    cyclic_term(Term)
  140    -> term_factorized(Term, Skel, Subst),
  141       Factorization = skel_subst(Skel, Subst)
  142    ;  Factorization = acyclic(Term).
  143
  144typecheck(Term, Type) :-
  145    $(copy_term(Term, Term_)),
  146    $(normalize(Type, CanonicalType)),
  147    cata(typecheck_, Term_, CanonicalType).
  148typecheck_(PreType, Type) =>
  149    % Try to look up the "full" type (if PreType is a function type then Type is too).
  150    functor(PreType, Ctor, _),
  151    get_possibly_cyclic_type(Ctor, FullPreType, FullType)
  152    *-> % Resolve Type to FullType, possibly prefixed with arrows if missing arguments.
  153	matchargs(PreType, Type, FullPreType, FullType)
  154    ;   % Otherwise, do an ad-hoc type declaration/skolemization.
  155	% This is similar to having declared
  156	% `same_functor(PreType, Skel), (type Skel ---> Skel)` ahead of time, so that
  157	% PreType is polymorphic in all arguments and has a unique type (the difference
  158        % is that the declaration would constrain the arity). In other words,
  159	% the ambient algebra is left free except where it has been explicitly
  160	% coalesced by declaring types with multiple ctors.
  161        $(\+ declared_type(PreType)), % Block skolemization when the term is a type, so that we can't inject into a type with the same functor as PreType.
  162	Type = PreType. % Skolemize.
  163
  164matchargs(PartTerm, PartType, FullTerm, FullType) :-
  165    $(PartTerm =.. [F|PartArgs]),
  166    $(FullTerm =.. [F|FullArgs]),
  167    append(PartArgs, RestArgs, FullArgs), % If RestArgs = [] then PartType = FullType.
  168    % PartType should be a chain of arrows through each of RestArgs before ending at FullType
  169    arrow_list(PartType, RestArgs, FullType).
  170
  171arrow_list(FullType, [], FullType).
  172arrow_list(X->Arrows, [X|List], RestArrows) :- arrow_list(Arrows, List, RestArrows)