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. 27:- dynamic alias_canonical/2. 28
29:- det((type)/1). 30
32type Type ---> PreTypes =>
33 $(nonvar(Type)),
34 $(nonvar(PreTypes)), 35 $(allowed_functor(Type)),
36 $(\+ declared_type(Type)), 37 $(\+ declared_ctor(Type)), 38 $(vars_preserved(PreTypes, Type)),
39 $(semicolon_list(PreTypes, PreTypeList)),
40 $(normalize(Type, NT)),
41 maplist(assert_type(NT), PreTypeList).
42
44type ---> PreType => type PreType ---> PreType.
45
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)), 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), 71 call(F, C, B),
72 mapargs(cata_(F, Seen1), A, C)
73 ; rb_lookup(A, B, Seen). 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)), 84 $(mapargs(normalize, PreType, NPT)), 85 $(functor(NPT, Ctor, _)),
86 $(assert_possibly_cyclic_type(Ctor, NPT, Type)). 87
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 \= (_ -> _), 102 Term \= please_evaluate_me_to(_). 103
104declared_type(Type) :-
105 $(same_functor(Type, Skel)), 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 150 functor(PreType, Ctor, _),
151 get_possibly_cyclic_type(Ctor, FullPreType, FullType)
152 *-> 153 matchargs(PreType, Type, FullPreType, FullType)
154 ; 155 156 157 158 159 160 161 $(\+ declared_type(PreType)), 162 Type = PreType. 163
164matchargs(PartTerm, PartType, FullTerm, FullType) :-
165 $(PartTerm =.. [F|PartArgs]),
166 $(FullTerm =.. [F|FullArgs]),
167 append(PartArgs, RestArgs, FullArgs), 168 169 arrow_list(PartType, RestArgs, FullType).
170
171arrow_list(FullType, [], FullType).
172arrow_list(X->Arrows, [X|List], RestArrows) :- arrow_list(Arrows, List, RestArrows)