97 (Binding.name_of name ^ " of " ^ (commas (map (print_anno_typ lthy) anno_tys)) ^ " " |
97 (Binding.name_of name ^ " of " ^ (commas (map (print_anno_typ lthy) anno_tys)) ^ " " |
98 ^ (commas (map print_bind bds)) ^ " " |
98 ^ (commas (map print_bind bds)) ^ " " |
99 ^ (Pretty.str_of (Syntax.pretty_mixfix syn))) |
99 ^ (Pretty.str_of (Syntax.pretty_mixfix syn))) |
100 *} |
100 *} |
101 |
101 |
102 ML Local_Theory.exit_global |
102 (* TODO: replace with the proper thing *) |
103 |
103 ML {* |
104 (* TODO: replace with proper thing *) |
104 fun is_atom ty = ty = "Test.name" |
105 ML {* |
105 *} |
106 fun is_atom ty = ty = "name" |
106 |
107 *} |
107 (* TODO: After variant_frees, check that the new names correspond to the ones given by user |
108 |
108 so that 'bind' is matched with variables correctly *) |
109 ML {* @{term "A \<union> B"} *} |
|
110 |
|
111 (* TODO: After variant_frees, check that the new names correspond to the ones given by user *) |
|
112 ML {* |
109 ML {* |
113 fun fv_constr lthy prefix dt_names (((name, anno_tys), bds), syn) = |
110 fun fv_constr lthy prefix dt_names (((name, anno_tys), bds), syn) = |
114 let |
111 let |
115 fun prepare_name (NONE, ty) = ("", ty) |
112 fun prepare_name (NONE, ty) = ("", ty) |
116 | prepare_name (SOME n, ty) = (n, ty); |
113 | prepare_name (SOME n, ty) = (n, ty); |
117 val vars = map Free (Variable.variant_frees lthy [] (map prepare_name anno_tys)); |
114 val vars = map Free (Variable.variant_frees lthy [] (map prepare_name anno_tys)); |
118 val var_strs = map (Syntax.string_of_term lthy) vars; |
115 val var_strs = map (Syntax.string_of_term lthy) vars; |
119 fun fv_var (t as Free (s, (ty as Type (tyS, _)))) = |
116 fun fv_var (t as Free (s, (ty as Type (tyS, _)))) = |
120 if is_atom tyS then HOLogic.mk_set ty [t] else |
117 if is_atom tyS then HOLogic.mk_set ty [t] else |
121 if tyS mem dt_names then Free ("fv_" ^ tyS, dummyT) $ t else |
118 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 |
122 @{term "{}"} |
120 @{term "{}"} |
123 val fv_eq = |
121 val fv_eq = |
124 if null vars then HOLogic.mk_set @{typ atom} [] |
122 if null vars then HOLogic.mk_set @{typ atom} [] |
125 else foldr1 (HOLogic.mk_binop @{const_name union}) (map fv_var vars) |
123 else foldr1 (HOLogic.mk_binop @{const_name union}) (map fv_var vars) |
126 val fv_eq_str = Syntax.string_of_term lthy fv_eq |
124 val fv_eq_str = Syntax.string_of_term lthy fv_eq |