1/* Part of typedef
    2	Copyright 2014-2015 Samer Abdallah (UCL)
    3
    4	This program is free software; you can redistribute it and/or
    5	modify it under the terms of the GNU Lesser General Public License
    6	as published by the Free Software Foundation; either version 2
    7	of the License, or (at your option) any later version.
    8
    9	This program is distributed in the hope that it will be useful,
   10	but WITHOUT ANY WARRANTY; without even the implied warranty of
   11	MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
   12	GNU Lesser General Public License for more details.
   13
   14	You should have received a copy of the GNU Lesser General Public
   15	License along with this library; if not, write to the Free Software
   16	Foundation, Inc., 51 Franklin Street, Fifth Floor, Boston, MA  02110-1301  USA
   17*/
   18
   19:- module(typedef,
   20    [ op(1150,fx,type)
   21    , op(1130,xfx,--->)
   22    , (type)/1
   23    , current_type/1
   24    , current_type_constructor/2
   25    ]).

Type definition framework

This module provides a way to declare new types that hook into the must_be/2 framework of library(error).

The type definition language is designed to be close to the one in Tom Schrijver's type_check package, supporting type synonyms, such as

:- type natnum == nonneg.

and algebraic type definitions like

:- type nat ---> zero ; succ(nat).

A built in type partial(T) is defined, which is satisfied by variables as well as terms that satisfy type T. This should be probably be extended to include all partial instantiations of type T, eg s(s(_)) should satisfy partial(nat), which it does not at the moment.

The result types can be used with must_be/2 and therefore in the record declarations provided by library(record) and the peristency declarations provided by library(persistency).

TODO

*/

   56:- multifile user_type_syn/2, user_type_def/1, user_type_constructor/2.   57:- multifile error:has_type/2.   58:- op(1150,fx,type).   59:- op(1130,xfx, --->).   60
   61% true if the module whose terms are being read has specifically
   62% imported library(typedef).
   63wants_typedef :-
   64   prolog_load_context(module, Module),
   65   Module \== typedef,  % we don't want typedef sugar ourselves
   66   predicate_property(Module:type(_),imported_from(typedef)).
   67
   68check_not_defined(Type) :-
   69   (  (user_type_syn(Type,_); user_type_def(Type))
   70   -> throw(error(duplicate_type(Type),(type)/1))
   71   ;  true
   72   ).
 type(Spec)
Declares a new type. Spec can be one of two forms: 
NewType ---> Constructor1 ; Constructor2 ; ... .
NewType == OldType

NewType can included type variables, which can be used in the constructor terms. The arguments of constructor terms are the types of the required arguments for that constructor. The second form declares a type synonym, so NewType is equivalent to OldType.

It is an error to declare the same type more than once, even if the definition is the same. Type name space is flat, not module scoped. This is directive. It cannot be called.

   88type(Spec) :- throw(error(context_error(nodirective, type(Spec)), _)).
 current_type(+Type) is semidet
current_type(-Type) is multi
True if Type is a currently defined type. For example, 
:- type foo ---> one ; two ; three.
:- type bar ---> hello ; goodbye.
?- current_type(Type).
Type = foo ;
Type = bar .
  100current_type(Type) :-
  101    user_type_def(Type).
 current_type_constructor(?T, ?Constructor)
True if a type T allows the Constructor. For example, 
:- type foo ---> one ; two ; three.
:- type bar ---> hello ; goodbye.
?- current_type_constructor(bar, C).
C = hello ;
C = goodbye .
  112current_type_constructor(Type, Constructor) :-
  113    user_type_constructor(Type, Constructor).
  114
  115system:term_expansion(:- type(Decl), Clauses) :-
  116   wants_typedef,
  117   (  expand_type_declaration(Decl, Clauses) -> true
  118   ;  throw(error(bad_type_declaration(Decl), (type)/1))
  119   ).
  120
  121expand_type_declaration(Type == Syn, [C1,C2]) :-
  122   % check_not_defined(Type),
  123   C1 = typedef:user_type_syn(Type,Syn),
  124   C2 = (error:has_type(Type, Value) :- error:has_type(Syn, Value)).
  125expand_type_declaration((Type ---> Defs), Clauses) :-
  126   % check_not_defined(Type),
  127   type_def(Type,Defs,Clauses,[]).
  128
  129type_def(Type,Defs) -->
  130   [ typedef:user_type_def(Type) ],
  131   [ error:has_type(Type, Value) :- typedef:has_type(Type,Value) ],
  132   constructors(Type,Defs).
  133
  134constructors(Type,C1;CX) --> !, constructor(Type,C1), constructors(Type,CX).
  135constructors(Type,CZ) --> constructor(Type,CZ).
  136constructor(Type,C) --> [ typedef:user_type_constructor(Type,C) ].
  137
  138error:has_type(partial(Type),Term) :- !,
  139   var(Term) -> true; error:has_type(Type,Term).
  140
  141has_type(Type,Term) :-
  142   user_type_def(Type), !, nonvar(Term),
  143   user_type_constructor(Type,Cons),
  144   (  atomic(Cons) -> Cons=Term
  145   ;  functor(Cons,F,A),
  146      functor(Term,F,A),
  147      forall( arg(N,Cons,ArgType), (arg(N,Term,ArgVal), error:has_type(ArgType,ArgVal)))
  148   ).
  149
  150prolog:message(error(duplicate_type(Type),_)) -->
  151   {numbervars(Type,0,_)},
  152   [ 'Redefinition of type ~w.'-[Type], nl]