1 theory Fv |
1 theory Fv |
2 imports "Nominal2_Atoms" "Abs" "Perm" "Rsp" |
2 imports "Nominal2_Atoms" "Abs" "Perm" "Rsp" |
3 begin |
3 begin |
4 |
4 |
5 (* TODO: update the comment *) |
5 (* Bindings are a list of lists of lists of triples. |
6 (* Bindings are given as a list which has a length being equal |
6 |
7 to the length of the number of constructors. |
7 The first list represents the datatypes defined. |
8 |
8 The second list represents the constructors. |
9 Each element is a list whose length is equal to the number |
9 The internal list is a list of all the bndings that |
10 of arguents. |
10 concern the constructor. |
11 |
11 |
12 Every element specifies bindings of this argument given as |
12 Every triple consists of a function, the binding and |
13 a tuple: function, bound argument. |
13 the body. |
14 |
14 |
15 Eg: |
15 Eg: |
16 nominal_datatype |
16 nominal_datatype |
17 |
17 |
18 C1 |
18 C1 |
20 | C3 x y z bind f x in z bind g y in z |
20 | C3 x y z bind f x in z bind g y in z |
21 |
21 |
22 yields: |
22 yields: |
23 [ |
23 [ |
24 [], |
24 [], |
25 [[], [], [(NONE, 0)]], |
25 [(NONE, 0, 2)], |
26 [[], [], [(SOME (Const f), 0), (Some (Const g), 1)]]] |
26 [(SOME (Const f), 0, 2), (Some (Const g), 1, 2)]] |
27 |
27 |
28 A SOME binding has to have a function returning an atom set, |
28 A SOME binding has to have a function which takes an appropriate |
29 and a NONE binding has to be on an argument that is an atom |
29 argument and returns an atom set. A NONE binding has to be on an |
30 or an atom set. |
30 argument that is an atom or an atom set. |
31 |
31 |
32 How the procedure works: |
32 How the procedure works: |
33 For each of the defined datatypes, |
33 For each of the defined datatypes, |
34 For each of the constructors, |
34 For each of the constructors, |
35 It creates a union of free variables for each argument. |
35 It creates a union of free variables for each argument. |
51 For an atom set, the atom set itself. |
51 For an atom set, the atom set itself. |
52 For a recursive argument, the appropriate fv function applied to it. |
52 For a recursive argument, the appropriate fv function applied to it. |
53 (* TODO: This one is not implemented *) |
53 (* TODO: This one is not implemented *) |
54 For other arguments it should be an appropriate fv function stored |
54 For other arguments it should be an appropriate fv function stored |
55 in the database. |
55 in the database. |
|
56 |
|
57 For every argument that is a binding, we add a the same binding in its |
|
58 body. |
56 *) |
59 *) |
57 |
60 |
|
61 (* Like map2, only if the second list is empty passes empty lists insted of error *) |
58 ML {* |
62 ML {* |
59 fun map2i _ [] [] = [] |
63 fun map2i _ [] [] = [] |
60 | map2i f (x :: xs) (y :: ys) = f x y :: map2i f xs ys |
64 | map2i f (x :: xs) (y :: ys) = f x y :: map2i f xs ys |
61 | map2i f (x :: xs) [] = f x [] :: map2i f xs [] |
65 | map2i f (x :: xs) [] = f x [] :: map2i f xs [] |
62 | map2i _ _ _ = raise UnequalLengths; |
66 | map2i _ _ _ = raise UnequalLengths; |
63 *} |
67 *} |
64 |
68 |
|
69 (* Finds bindings with the same function and binding, and gathers all |
|
70 bodys for such pairs *) |
65 ML {* |
71 ML {* |
66 fun gather_binds binds = |
72 fun gather_binds binds = |
67 let |
73 let |
68 fun gather_binds_cons binds = |
74 fun gather_binds_cons binds = |
69 let |
75 let |