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 (* Bindings are a list of lists of lists of triples. |
5 (* The bindings data structure: |
|
6 |
|
7 Bindings are a list of lists of lists of triples. |
6 |
8 |
7 The first list represents the datatypes defined. |
9 The first list represents the datatypes defined. |
8 The second list represents the constructors. |
10 The second list represents the constructors. |
9 The internal list is a list of all the bndings that |
11 The internal list is a list of all the bndings that |
10 concern the constructor. |
12 concern the constructor. |
26 [(SOME (Const f), 0, 2), (Some (Const g), 1, 2)]] |
28 [(SOME (Const f), 0, 2), (Some (Const g), 1, 2)]] |
27 |
29 |
28 A SOME binding has to have a function which takes an appropriate |
30 A SOME binding has to have a function which takes an appropriate |
29 argument and returns an atom set. A NONE binding has to be on an |
31 argument and returns an atom set. A NONE binding has to be on an |
30 argument that is an atom or an atom set. |
32 argument that is an atom or an atom set. |
31 |
33 *) |
32 How the procedure works: |
34 |
33 For each of the defined datatypes, |
35 (* |
34 For each of the constructors, |
36 The overview of the generation of free variables: |
35 It creates a union of free variables for each argument. |
37 |
36 |
38 1) fv_bn functions are generated only for the non-recursive binds. |
37 For an argument the free variables are the variables minus |
39 |
38 bound variables. |
40 An fv_bn for a constructor is a union of values for the arguments: |
39 |
41 |
40 The variables are: |
42 For an argument x that is in the bn function |
41 For an atom, a singleton set with the atom itself. |
43 - if it is a recursive argument bn' we return: fv_bn' x |
42 For an atom set, the atom set itself. |
44 - otherwise empty |
43 For a recursive argument, the appropriate fv function applied to it. |
45 |
44 (* TODO: This one is not implemented *) |
46 For an argument x that is not in the bn function |
45 For other arguments it should be an appropriate fv function stored |
47 - for atom we return: {atom x} |
46 in the database. |
48 - for atom set we return: atom ` x |
47 The bound variables are a union of results of all bindings that |
49 - for a recursive call to type ty' we return: fv_ty' x |
48 involve the given argument. For a paricular binding the result is: |
50 with fv of the appropriate type |
49 For a function applied to an argument this function with the argument. |
51 - otherwise empty |
50 For an atom, a singleton set with the atom itself. |
52 |
51 For an atom set, the atom set itself. |
53 2) fv functions generated for all new datatypes: |
52 For a recursive argument, the appropriate fv function applied to it. |
54 |
53 (* TODO: This one is not implemented *) |
55 An fv for a constructor is a union of values for the arguments. |
54 For other arguments it should be an appropriate fv function stored |
56 |
55 in the database. |
57 For an argument x that bound in a non-recursive binding |
56 |
58 we return: fv_bn x. |
57 For every argument that is a binding, we add a the same binding in its |
59 |
58 body. |
60 Otherwise we return the free variables of the argument minus the |
|
61 bound variables of the argument. |
|
62 |
|
63 The free variables for an argument x are: |
|
64 - for an atom: {atom x} |
|
65 - for atom set: atom ` x |
|
66 - for recursive call to type ty' return: fv_ty' x |
|
67 - for nominal datatype ty' return: fv_ty' x |
|
68 |
|
69 The bound variables are a union of results of all bindings that |
|
70 involve the given argument. For a paricular binding: |
|
71 |
|
72 - for a binding function bn: bn x |
|
73 - for an atom: {atom x} |
|
74 - for atom set: atom ` x |
|
75 - for a recursive argument of type ty': fv_fy' x |
|
76 - for nominal datatype ty' return: fv_ty' x |
59 *) |
77 *) |
60 |
78 |
61 ML {* |
79 ML {* |
62 fun is_atom thy typ = |
80 fun is_atom thy typ = |
63 Sign.of_sort thy (typ, @{sort at}) |
81 Sign.of_sort thy (typ, @{sort at}) |
186 distinct (op =) (map_filter is_non_rec (flat (flat l))) |
204 distinct (op =) (map_filter is_non_rec (flat (flat l))) |
187 end |
205 end |
188 *} |
206 *} |
189 |
207 |
190 (* We assume no bindings in the type on which bn is defined *) |
208 (* We assume no bindings in the type on which bn is defined *) |
|
209 (* TODO: currently works only with current fv_bn function *) |
191 ML {* |
210 ML {* |
192 fun fv_bn thy (dt_info : Datatype_Aux.info) fv_frees (bn, ith_dtyp, args_in_bns) = |
211 fun fv_bn thy (dt_info : Datatype_Aux.info) fv_frees (bn, ith_dtyp, args_in_bns) = |
193 let |
212 let |
194 val {descr, sorts, ...} = dt_info; |
213 val {descr, sorts, ...} = dt_info; |
195 fun nth_dtyp i = typ_of_dtyp descr sorts (DtRec i); |
214 fun nth_dtyp i = typ_of_dtyp descr sorts (DtRec i); |
329 @{term "{} :: atom set"} |
348 @{term "{} :: atom set"} |
330 | fv_bind args (SOME (f, _), i, _) = f $ (nth args i); |
349 | fv_bind args (SOME (f, _), i, _) = f $ (nth args i); |
331 fun fv_binds args relevant = mk_union (map (fv_bind args) relevant) |
350 fun fv_binds args relevant = mk_union (map (fv_bind args) relevant) |
332 fun find_nonrec_binder j (SOME (f, false), i, _) = if i = j then SOME f else NONE |
351 fun find_nonrec_binder j (SOME (f, false), i, _) = if i = j then SOME f else NONE |
333 | find_nonrec_binder _ _ = NONE |
352 | find_nonrec_binder _ _ = NONE |
334 fun find_compound_binder j (SOME (f, r), i, _) = if i = j then SOME (f, r) else NONE |
|
335 | find_compound_binder _ _ = NONE |
|
336 fun fv_arg ((dt, x), arg_no) = |
353 fun fv_arg ((dt, x), arg_no) = |
337 case get_first (find_nonrec_binder arg_no) bindcs of |
354 case get_first (find_nonrec_binder arg_no) bindcs of |
338 SOME f => |
355 SOME f => |
339 (case get_first (fn (x, y) => if x = f then SOME y else NONE) bn_fv_bns of |
356 (case get_first (fn (x, y) => if x = f then SOME y else NONE) bn_fv_bns of |
340 SOME fv_bn => fv_bn $ x |
357 SOME fv_bn => fv_bn $ x |