45 |
45 |
46 (* functions for producing sets, fsets and lists *) |
46 (* functions for producing sets, fsets and lists *) |
47 fun mk_atom_set t = |
47 fun mk_atom_set t = |
48 let |
48 let |
49 val ty = fastype_of t; |
49 val ty = fastype_of t; |
50 val atom_ty = HOLogic.dest_setT ty --> @{typ atom}; |
50 val atom_ty = HOLogic.dest_setT ty --> @{typ "atom"}; |
51 val img_ty = atom_ty --> ty --> @{typ "atom set"}; |
51 val img_ty = atom_ty --> ty --> @{typ "atom set"}; |
52 in |
52 in |
53 (Const (@{const_name image}, img_ty) $ mk_atom_ty atom_ty t) |
53 (Const (@{const_name image}, img_ty) $ mk_atom_ty atom_ty t) |
54 end; |
54 end; |
55 |
55 |
56 fun mk_atom_fset t = |
56 fun mk_atom_fset t = |
57 let |
57 let |
58 val ty = fastype_of t; |
58 val ty = fastype_of t; |
59 val atom_ty = dest_fsetT ty --> @{typ atom}; |
59 val atom_ty = dest_fsetT ty --> @{typ "atom"}; |
60 val fmap_ty = atom_ty --> ty --> @{typ "atom fset"}; |
60 val fmap_ty = atom_ty --> ty --> @{typ "atom fset"}; |
61 val fset_to_set = @{term "fset_to_set :: atom fset => atom set"} |
61 val fset_to_set = @{term "fset_to_set :: atom fset => atom set"} |
62 in |
62 in |
63 fset_to_set $ (Const (@{const_name fmap}, fmap_ty) $ Const (@{const_name atom}, atom_ty) $ t) |
63 fset_to_set $ (Const (@{const_name fmap}, fmap_ty) $ Const (@{const_name atom}, atom_ty) $ t) |
64 end; |
64 end; |
65 |
65 |
|
66 (* |
66 fun mk_atom_list t = |
67 fun mk_atom_list t = |
67 let |
68 let |
68 val ty = fastype_of t; |
69 val ty = fastype_of t; |
69 val atom_ty = dest_listT ty --> @{typ atom}; |
70 val atom_ty = dest_listT ty --> @{typ atom}; |
70 val map_ty = atom_ty --> ty --> @{typ "atom list"}; |
71 val map_ty = atom_ty --> ty --> @{typ "atom list"}; |
71 in |
72 in |
72 (Const (@{const_name map}, map_ty) $ mk_atom_ty atom_ty t) |
73 (Const (@{const_name map}, map_ty) $ mk_atom_ty atom_ty t) |
73 end; |
74 end; |
74 |
75 *) |
75 |
76 |
76 (* functions that coerces atoms, sets and fsets into atom sets ? *) |
77 (* functions that coerces atoms, sets and fsets into atom sets ? *) |
77 fun setify ctxt t = |
78 fun setify ctxt t = |
78 let |
79 let |
79 val ty = fastype_of t; |
80 val ty = fastype_of t; |
98 then mk_atom_set t |
99 then mk_atom_set t |
99 else raise TERM ("listify", [t]) |
100 else raise TERM ("listify", [t]) |
100 end |
101 end |
101 |
102 |
102 (* coerces a list into a set *) |
103 (* coerces a list into a set *) |
103 fun to_set x = |
104 fun to_set t = |
104 if fastype_of x = @{typ "atom list"} |
105 if fastype_of t = @{typ "atom list"} |
105 then @{term "set::atom list => atom set"} $ x |
106 then @{term "set::atom list => atom set"} $ t |
106 else x |
107 else t |
107 |
108 |
108 |
109 |
109 |
110 (* functions that construct the equations for fv and fv_bn *) |
110 fun make_body fv_map args i = |
111 |
|
112 fun make_fv_body fv_map args i = |
111 let |
113 let |
112 val arg = nth args i |
114 val arg = nth args i |
113 val ty = fastype_of arg |
115 val ty = fastype_of arg |
114 in |
116 in |
115 case (AList.lookup (op=) fv_map ty) of |
117 case (AList.lookup (op=) fv_map ty) of |
116 NONE => mk_supp arg |
118 NONE => mk_supp arg |
117 | SOME fv => fv $ arg |
119 | SOME fv => fv $ arg |
118 end |
120 end |
119 |
121 |
120 fun make_binder lthy fv_bn_map args (bn_option, i) = |
122 fun make_fv_binder lthy fv_bn_map args (bn_option, i) = |
121 let |
123 let |
122 val arg = nth args i |
124 val arg = nth args i |
123 in |
125 in |
124 case bn_option of |
126 case bn_option of |
125 NONE => (setify lthy arg, @{term "{}::atom set"}) |
127 NONE => (setify lthy arg, @{term "{}::atom set"}) |
126 | SOME bn => (to_set (bn $ arg), the (AList.lookup (op=) fv_bn_map bn) $ arg) |
128 | SOME bn => (to_set (bn $ arg), the (AList.lookup (op=) fv_bn_map bn) $ arg) |
127 end |
129 end |
128 |
130 |
129 fun make_fv_rhs lthy fv_map fv_bn_map args (BC (_, binders, bodies)) = |
131 fun make_fv_rhs lthy fv_map fv_bn_map args (BC (_, binders, bodies)) = |
130 let |
132 let |
131 val t1 = map (make_body fv_map args) bodies |
133 val t1 = map (make_fv_body fv_map args) bodies |
132 val (t2, t3) = split_list (map (make_binder lthy fv_bn_map args) binders) |
134 val (t2, t3) = split_list (map (make_fv_binder lthy fv_bn_map args) binders) |
133 in |
135 in |
134 fold_union (mk_diff (fold_union t1, fold_union t2)::t3) |
136 fold_union (mk_diff (fold_union t1, fold_union t2)::t3) |
135 end |
137 end |
136 |
138 |
137 fun make_fv_eq lthy fv_map fv_bn_map (constr, ty, arg_tys) bclauses = |
139 fun make_fv_eq lthy fv_map fv_bn_map (constr, ty, arg_tys) bclauses = |
160 | SOME (SOME bn) => the (AList.lookup (op=) fv_bn_map bn) $ arg |
162 | SOME (SOME bn) => the (AList.lookup (op=) fv_bn_map bn) $ arg |
161 end |
163 end |
162 |
164 |
163 fun make_fv_bn_rhs lthy fv_map fv_bn_map bn_args args bclause = |
165 fun make_fv_bn_rhs lthy fv_map fv_bn_map bn_args args bclause = |
164 case bclause of |
166 case bclause of |
165 BC (_, [], bodies) => fold_union (map (make_bn_body fv_map fv_bn_map bn_args args) bodies) |
167 BC (_, [], bodies) => fold_union (map (make_fv_bn_body fv_map fv_bn_map bn_args args) bodies) |
166 | BC (_, binders, bodies) => |
168 | BC (_, binders, bodies) => |
167 let |
169 let |
168 val t1 = map (make_body fv_map args) bodies |
170 val t1 = map (make_fv_body fv_map args) bodies |
169 val (t2, t3) = split_list (map (make_binder lthy fv_bn_map args) binders) |
171 val (t2, t3) = split_list (map (make_fv_binder lthy fv_bn_map args) binders) |
170 in |
172 in |
171 fold_union (mk_diff (fold_union t1, fold_union t2)::t3) |
173 fold_union (mk_diff (fold_union t1, fold_union t2)::t3) |
172 end |
174 end |
173 |
175 |
174 fun make_fv_bn_eq lthy bn_trm fv_map fv_bn_map (bn_args, (constr, ty, arg_tys)) bclauses = |
176 fun make_fv_bn_eq lthy bn_trm fv_map fv_bn_map (bn_args, (constr, _, arg_tys)) bclauses = |
175 let |
177 let |
176 val arg_names = Datatype_Prop.make_tnames arg_tys |
178 val arg_names = Datatype_Prop.make_tnames arg_tys |
177 val args = map Free (arg_names ~~ arg_tys) |
179 val args = map Free (arg_names ~~ arg_tys) |
178 val fv_bn = the (AList.lookup (op=) fv_bn_map bn_trm) |
180 val fv_bn = the (AList.lookup (op=) fv_bn_map bn_trm) |
179 val lhs = fv_bn $ list_comb (constr, args) |
181 val lhs = fv_bn $ list_comb (constr, args) |