1/*
2 * Code for inferring monotypes for programs in the simple
3 * functional programming language
4 */
5
6module monoinfer.
7
8accum_sig  pcf, monotypes.
9
10type prim, infer      tm -> ty -> o.
11
12infer (M @ N) B        :- infer M (A --> B), infer N A.
13infer (fn M) (A --> B) :- pi x\ infer x A => infer (M x) B.
14infer (fixpt M) A      :- pi x\ infer x A => infer (M x) A.
15infer (cond C T E) A   :- infer C bool, infer T A, infer E A.
16infer T A              :- prim T A.
17
18% Primitive for lists.
19
20prim car    ((lst A) --> A).
21prim cdr    ((lst A) --> (lst A) ).
22prim empty  (lst A).
23prim cons   (A --> (lst A) --> (lst A) ).
24prim nullp  ((lst A) --> bool).
25prim consp  ((lst A) --> bool).
26
27% Primitives for booleans.
28
29prim equal  (A --> A --> bool).
30prim and    (bool --> bool --> bool).
31prim or     (bool --> bool --> bool).
32prim truth   bool.
33prim false   bool.
34
35% Primitives for integers
36
37prim times    (num --> num --> num).
38prim plus     (num --> num --> num).
39prim minus    (num --> num --> num).
40prim zerop    (num --> bool).
41prim greater  (num --> num --> bool).
42prim (in N)    num.
43