26 |
26 |
27 A SOME binding has to have a function returning an atom set, |
27 A SOME binding has to have a function returning an atom set, |
28 and a NONE binding has to be on an argument that is an atom |
28 and a NONE binding has to be on an argument that is an atom |
29 or an atom set. |
29 or an atom set. |
30 |
30 |
|
31 How the procedure works: |
|
32 For each of the defined datatypes, |
|
33 For each of the constructors, |
|
34 It creates a union of free variables for each argument. |
|
35 |
|
36 For an argument the free variables are the variables minus |
|
37 bound variables. |
|
38 |
|
39 The variables are: |
|
40 For an atom, a singleton set with the atom itself. |
|
41 For an atom set, the atom set itself. |
|
42 For a recursive argument, the appropriate fv function applied to it. |
|
43 (* TODO: This one is not implemented *) |
|
44 For other arguments it should be an appropriate fv function stored |
|
45 in the database. |
|
46 The bound variables are a union of results of all bindings that |
|
47 involve the given argument. For a paricular binding the result is: |
|
48 For a function applied to an argument this function with the argument. |
|
49 For an atom, a singleton set with the atom itself. |
|
50 For an atom set, the atom set itself. |
|
51 For a recursive argument, the appropriate fv function applied to it. |
|
52 (* TODO: This one is not implemented *) |
|
53 For other arguments it should be an appropriate fv function stored |
|
54 in the database. |
31 *) |
55 *) |
32 |
56 |
33 ML {* |
57 ML {* |
34 open Datatype_Aux; (* typ_of_dtyp, DtRec, ... *); |
58 open Datatype_Aux; (* typ_of_dtyp, DtRec, ... *); |
35 (* TODO: It is the same as one in 'nominal_atoms' *) |
59 (* TODO: It is the same as one in 'nominal_atoms' *) |