equal
deleted
inserted
replaced
11 |
11 |
12 TODO: optimize red by special-casing it |
12 TODO: optimize red by special-casing it |
13 *) |
13 *) |
14 |
14 |
15 signature PATTERN = |
15 signature PATTERN = |
16 sig |
16 sig |
17 type type_sig |
17 type type_sig |
18 type sg |
18 type sg |
19 type env |
19 type env |
20 val eta_contract: term -> term |
20 val eta_contract: term -> term |
21 val match: type_sig -> term * term |
21 val match: type_sig -> term * term |
23 val matches: type_sig -> term * term -> bool |
23 val matches: type_sig -> term * term -> bool |
24 val unify: sg * env * (term * term)list -> env |
24 val unify: sg * env * (term * term)list -> env |
25 exception Unif |
25 exception Unif |
26 exception MATCH |
26 exception MATCH |
27 exception Pattern |
27 exception Pattern |
28 end; |
28 end; |
29 |
29 |
30 functor PatternFun(structure Sign:SIGN and Envir:ENVIR): PATTERN = |
30 structure Pattern : PATTERN = |
31 struct |
31 struct |
32 |
|
33 structure Type = Sign.Type; |
|
34 |
32 |
35 type type_sig = Type.type_sig |
33 type type_sig = Type.type_sig |
36 type sg = Sign.sg |
34 type sg = Sign.sg |
37 type env = Envir.env |
35 type env = Envir.env |
38 |
36 |