93 in |
93 in |
94 if i = 0 then Mixfix (syn, [], 1000) |
94 if i = 0 then Mixfix (syn, [], 1000) |
95 else Mixfix (syn ^ "()'(/" ^ args ^ "')", replicate i 0, 1000) |
95 else Mixfix (syn ^ "()'(/" ^ args ^ "')", replicate i 0, 1000) |
96 end |
96 end |
97 |
97 |
98 fun process_attributes T = |
98 fun maybe_builtin T = |
99 let |
99 let |
100 fun const name = SOME (Const (name, T)) |
100 fun const name = SOME (Const (name, T)) |
101 |
101 |
102 fun choose builtin = |
102 fun choose builtin = |
103 (case builtin of |
103 (case builtin of |
150 let val isa_name = isabelle_name name and U = Ts ---> T |
150 let val isa_name = isabelle_name name and U = Ts ---> T |
151 in |
151 in |
152 (case lookup_const thy isa_name U of |
152 (case lookup_const thy isa_name U of |
153 SOME t => (((name, t), false), thy) |
153 SOME t => (((name, t), false), thy) |
154 | NONE => |
154 | NONE => |
155 (case process_attributes U atts of |
155 (case maybe_builtin U atts of |
156 SOME t => (((name, t), false), thy) |
156 SOME t => (((name, t), false), thy) |
157 | NONE => |
157 | NONE => |
158 thy |
158 thy |
159 |> Sign.declare_const ((Binding.name isa_name, U), |
159 |> Sign.declare_const ((Binding.name isa_name, U), |
160 mk_syntax name (length Ts)) |
160 mk_syntax name (length Ts)) |
161 |> apfst (rpair true o pair name))) |
161 |> apfst (rpair true o pair name))) |
162 end |
162 end |
163 |
163 |
164 fun const_names ((name, _), ((_, t), new)) = |
164 fun new_names ((name, t), new) = |
165 if new then SOME (fst (Term.dest_Const t) ^ " (as " ^ name ^ ")") else NONE |
165 if new then SOME (fst (Term.dest_Const t) ^ " (as " ^ name ^ ")") else NONE |
|
166 |
|
167 fun uniques fns fds = |
|
168 let |
|
169 fun is_unique (name, (([], T), atts)) = |
|
170 (case AList.lookup (op =) atts "unique" of |
|
171 SOME _ => Symtab.lookup fds name |
|
172 | NONE => NONE) |
|
173 | is_unique _ = NONE |
|
174 fun mk_unique_axiom T ts = |
|
175 Const (@{const_name distinct}, HOLogic.listT T --> @{typ bool}) $ |
|
176 HOLogic.mk_list T ts |
|
177 in |
|
178 map_filter is_unique fns |
|
179 |> map (swap o Term.dest_Const) |
|
180 |> AList.group (op =) |
|
181 |> map (fn (T, ns) => mk_unique_axiom T (map (Const o rpair T) ns)) |
|
182 end |
166 in |
183 in |
167 fun declare_functions verbose fns = |
184 fun declare_functions verbose fns = |
168 fold_map declare fns #-> (fn fds => |
185 fold_map declare fns #-> (fn fds => |
169 log verbose "Declared constants:" (map_filter const_names (fns ~~ fds)) #> |
186 log verbose "Declared constants:" (map_filter new_names fds) #> |
170 rpair (Symtab.make (map fst fds))) |
187 rpair (` (uniques fns) (Symtab.make (map fst fds)))) |
171 end |
188 end |
172 |
189 |
173 |
190 |
174 |
191 |
175 local |
192 local |
490 (fn ((name, arity), i) => |
507 (fn ((name, arity), i) => |
491 scan_count (typ tds) (arity - 1) -- typ tds -- |
508 scan_count (typ tds) (arity - 1) -- typ tds -- |
492 scan_count (attribute tds Symtab.empty) i >> pair name)) >> |
509 scan_count (attribute tds Symtab.empty) i >> pair name)) >> |
493 (fn fns => declare_functions verbose fns thy)) |
510 (fn fns => declare_functions verbose fns thy)) |
494 |
511 |
495 fun axioms verbose tds fds = Scan.depend (fn thy => |
512 fun axioms verbose tds fds unique_axs = Scan.depend (fn thy => |
496 Scan.repeat (scan_line "axiom" num :|-- (fn i => |
513 Scan.repeat (scan_line "axiom" num :|-- (fn i => |
497 expr tds fds --| scan_count (attribute tds fds) i)) >> |
514 expr tds fds --| scan_count (attribute tds fds) i)) >> |
498 (fn axs => (add_axioms verbose axs thy, ()))) |
515 (fn axs => (add_axioms verbose (unique_axs @ axs) thy, ()))) |
499 |
516 |
500 fun var_decls tds fds = Scan.depend (fn thy => |
517 fun var_decls tds fds = Scan.depend (fn thy => |
501 Scan.repeat (scan_line "var-decl" (str -- num) :|-- (fn (_, i) => |
518 Scan.repeat (scan_line "var-decl" (str -- num) :|-- (fn (_, i) => |
502 typ tds -- scan_count (attribute tds fds) i >> K ())) >> K (thy, ())) |
519 typ tds -- scan_count (attribute tds fds) i >> K ())) >> K (thy, ())) |
503 |
520 |
506 (expr tds fds >> Sign.cert_term thy)) >> |
523 (expr tds fds >> Sign.cert_term thy)) >> |
507 (fn vcs => ((), add_vcs verbose vcs thy))) |
524 (fn vcs => ((), add_vcs verbose vcs thy))) |
508 |
525 |
509 fun parse verbose thy = Scan.pass thy |
526 fun parse verbose thy = Scan.pass thy |
510 (type_decls verbose :|-- (fn tds => |
527 (type_decls verbose :|-- (fn tds => |
511 fun_decls verbose tds :|-- (fn fds => |
528 fun_decls verbose tds :|-- (fn (unique_axs, fds) => |
512 axioms verbose tds fds |-- |
529 axioms verbose tds fds unique_axs |-- |
513 var_decls tds fds |-- |
530 var_decls tds fds |-- |
514 vcs verbose tds fds))) |
531 vcs verbose tds fds))) |
515 |
532 |
516 fun load_b2i verbose path thy = finite (parse verbose thy) path |
533 fun load_b2i verbose path thy = finite (parse verbose thy) path |
517 |
534 |