19 @{index_ML Variable.polymorphic: "Proof.context -> term list -> term list"} \\ |
19 @{index_ML Variable.polymorphic: "Proof.context -> term list -> term list"} \\ |
20 \end{mldecls} |
20 \end{mldecls} |
21 |
21 |
22 \begin{description} |
22 \begin{description} |
23 |
23 |
24 \item @{ML Variable.declare_term} FIXME |
24 \item @{ML Variable.declare_term} declares a term as belonging to |
|
25 the current context. This fixes free type variables, but not term |
|
26 variables; constraints for type and term variables are declared |
|
27 uniformly. |
25 |
28 |
26 \item @{ML Variable.import} FIXME |
29 \item @{ML Variable.import} introduces new fixes for schematic type |
|
30 and term variables occurring in given facts. The effect may be |
|
31 reversed (up to renaming) via @{ML Variable.export}. |
27 |
32 |
28 \item @{ML Variable.export} FIXME |
33 \item @{ML Variable.export} generalizes fixed type and term |
|
34 variables according to the difference of the two contexts. Note |
|
35 that type variables occurring in term variables are still fixed, |
|
36 even though they got introduced later (e.g.\ by type-inference). |
29 |
37 |
30 \item @{ML Variable.trade} composes @{ML Variable.import} and @{ML |
38 \item @{ML Variable.trade} composes @{ML Variable.import} and @{ML |
31 Variable.export}. |
39 Variable.export}, i.e.\ it provides a view on facts with all |
|
40 variables being fixed in the current context. |
32 |
41 |
33 \item @{ML Variable.monomorphic} FIXME |
42 \item @{ML Variable.monomorphic} introduces fixed type variables for |
|
43 the schematic of the given facts. |
34 |
44 |
35 \item @{ML Variable.polymorphic} FIXME |
45 \item @{ML Variable.polymorphic} generalizes type variables as far |
|
46 as possible, even those occurring in fixed term variables. This |
|
47 operation essentially reverses the default policy of type-inference |
|
48 to introduce local polymorphism entities in fixed form. |
36 |
49 |
37 \end{description} |
50 \end{description} |
38 *} |
51 *} |
39 |
52 |
40 text FIXME |
53 text FIXME |