102 (* TODO: replace with the proper thing *) |
102 (* TODO: replace with the proper thing *) |
103 ML {* |
103 ML {* |
104 fun is_atom ty = ty = "Test.name" |
104 fun is_atom ty = ty = "Test.name" |
105 *} |
105 *} |
106 |
106 |
|
107 ML {* |
|
108 fun fv_bds s bds set = |
|
109 case bds of |
|
110 [] => set |
|
111 | B (s1, s2) :: tl => |
|
112 if s2 = s then |
|
113 fv_bds s tl (HOLogic.mk_binop @{const_name "HOL.minus_class.minus"} (set, HOLogic.mk_set @{typ name} [Free (s1, @{typ name})])) |
|
114 else fv_bds s tl set |
|
115 | BS (s1, s2) :: tl => |
|
116 (* TODO: This is just a copy *) |
|
117 if s2 = s then |
|
118 fv_bds s tl (HOLogic.mk_binop @{const_name "HOL.minus_class.minus"} (set, HOLogic.mk_set @{typ name} [Free (s1, @{typ name})])) |
|
119 else fv_bds s tl set |
|
120 *} |
|
121 |
107 (* TODO: After variant_frees, check that the new names correspond to the ones given by user |
122 (* TODO: After variant_frees, check that the new names correspond to the ones given by user |
108 so that 'bind' is matched with variables correctly *) |
123 so that 'bind' is matched with variables correctly *) |
109 ML {* |
124 ML {* |
110 fun fv_constr lthy prefix dt_names (((name, anno_tys), bds), syn) = |
125 fun fv_constr lthy prefix dt_names (((name, anno_tys), bds), syn) = |
111 let |
126 let |
113 | prepare_name (SOME n, ty) = (n, ty); |
128 | prepare_name (SOME n, ty) = (n, ty); |
114 val vars = map Free (Variable.variant_frees lthy [] (map prepare_name anno_tys)); |
129 val vars = map Free (Variable.variant_frees lthy [] (map prepare_name anno_tys)); |
115 val var_strs = map (Syntax.string_of_term lthy) vars; |
130 val var_strs = map (Syntax.string_of_term lthy) vars; |
116 fun fv_var (t as Free (s, (ty as Type (tyS, _)))) = |
131 fun fv_var (t as Free (s, (ty as Type (tyS, _)))) = |
117 if is_atom tyS then HOLogic.mk_set ty [t] else |
132 if is_atom tyS then HOLogic.mk_set ty [t] else |
118 if (Long_Name.base_name tyS) mem dt_names then |
133 if (Long_Name.base_name tyS) mem dt_names then |
119 Free ("fv_" ^ (Long_Name.base_name tyS), Type ("fun", [dummyT, @{typ "name set"}])) $ t else |
134 fv_bds s bds (Free ("fv_" ^ (Long_Name.base_name tyS), Type ("fun", [dummyT, @{typ "name set"}])) $ t) else |
120 HOLogic.mk_set @{typ name} [] |
135 HOLogic.mk_set @{typ name} [] |
121 val fv_eq = |
136 val fv_eq = |
122 if null vars then HOLogic.mk_set @{typ name} [] |
137 if null vars then HOLogic.mk_set @{typ name} [] |
123 else foldr1 (HOLogic.mk_binop @{const_name union}) (map fv_var vars) |
138 else foldr1 (HOLogic.mk_binop @{const_name union}) (map fv_var vars) |
124 val fv_eq_str = Syntax.string_of_term lthy (Syntax.check_term lthy fv_eq) |
139 val fv_eq_str = Syntax.string_of_term lthy (Syntax.check_term lthy fv_eq) |
125 in |
140 in |
126 prefix ^ " (" ^ (Binding.name_of name) ^ " " ^ (implode (separate " " var_strs)) ^ ") = " ^ fv_eq_str |
141 prefix ^ " (" ^ (Binding.name_of name) ^ " " ^ (implode (separate " " var_strs)) ^ ") = " ^ fv_eq_str |