425 fun find_name [] = sys_error "mk_long_id" |
425 fun find_name [] = sys_error "mk_long_id" |
426 | find_name (ys :: yss) = |
426 | find_name (ys :: yss) = |
427 let |
427 let |
428 val s' = NameSpace.pack ys |
428 val s' = NameSpace.pack ys |
429 val s'' = NameSpace.append module s' |
429 val s'' = NameSpace.append module s' |
430 in case Symtab.lookup (used, s'') of |
430 in case Symtab.curried_lookup used s'' of |
431 NONE => ((module, s'), (Symtab.update_new ((s, (module, s')), tab), |
431 NONE => ((module, s'), |
432 Symtab.update_new ((s'', ()), used))) |
432 (Symtab.curried_update_new (s, (module, s')) tab, |
|
433 Symtab.curried_update_new (s'', ()) used)) |
433 | SOME _ => find_name yss |
434 | SOME _ => find_name yss |
434 end |
435 end |
435 in case Symtab.lookup (tab, s) of |
436 in case Symtab.curried_lookup tab s of |
436 NONE => find_name (Library.suffixes1 (NameSpace.unpack s)) |
437 NONE => find_name (Library.suffixes1 (NameSpace.unpack s)) |
437 | SOME name => (name, p) |
438 | SOME name => (name, p) |
438 end; |
439 end; |
439 |
440 |
440 (* module: module name for caller *) |
441 (* module: module name for caller *) |
450 val s' = mk_id s; |
451 val s' = mk_id s; |
451 val s'' = if s' mem ThmDatabase.ml_reserved then s' ^ "_const" else s' |
452 val s'' = if s' mem ThmDatabase.ml_reserved then s' ^ "_const" else s' |
452 in ((gr, (tab1', tab2)), (module, s'')) end; |
453 in ((gr, (tab1', tab2)), (module, s'')) end; |
453 |
454 |
454 fun get_const_id cname (gr, (tab1, tab2)) = |
455 fun get_const_id cname (gr, (tab1, tab2)) = |
455 case Symtab.lookup (fst tab1, cname) of |
456 case Symtab.curried_lookup (fst tab1) cname of |
456 NONE => error ("get_const_id: no such constant: " ^ quote cname) |
457 NONE => error ("get_const_id: no such constant: " ^ quote cname) |
457 | SOME (module, s) => |
458 | SOME (module, s) => |
458 let |
459 let |
459 val s' = mk_id s; |
460 val s' = mk_id s; |
460 val s'' = if s' mem ThmDatabase.ml_reserved then s' ^ "_const" else s' |
461 val s'' = if s' mem ThmDatabase.ml_reserved then s' ^ "_const" else s' |
466 val s' = mk_id s; |
467 val s' = mk_id s; |
467 val s'' = if s' mem ThmDatabase.ml_reserved then s' ^ "_type" else s' |
468 val s'' = if s' mem ThmDatabase.ml_reserved then s' ^ "_type" else s' |
468 in ((gr, (tab1, tab2')), (module, s'')) end; |
469 in ((gr, (tab1, tab2')), (module, s'')) end; |
469 |
470 |
470 fun get_type_id tyname (gr, (tab1, tab2)) = |
471 fun get_type_id tyname (gr, (tab1, tab2)) = |
471 case Symtab.lookup (fst tab2, tyname) of |
472 case Symtab.curried_lookup (fst tab2) tyname of |
472 NONE => error ("get_type_id: no such type: " ^ quote tyname) |
473 NONE => error ("get_type_id: no such type: " ^ quote tyname) |
473 | SOME (module, s) => |
474 | SOME (module, s) => |
474 let |
475 let |
475 val s' = mk_id s; |
476 val s' = mk_id s; |
476 val s'' = if s' mem ThmDatabase.ml_reserved then s' ^ "_type" else s' |
477 val s'' = if s' mem ThmDatabase.ml_reserved then s' ^ "_type" else s' |
554 end handle TERM _ => NONE; |
555 end handle TERM _ => NONE; |
555 fun add_def thyname (defs, (name, t)) = (case dest t of |
556 fun add_def thyname (defs, (name, t)) = (case dest t of |
556 NONE => defs |
557 NONE => defs |
557 | SOME _ => (case dest (prep_def (Thm.get_axiom thy name)) of |
558 | SOME _ => (case dest (prep_def (Thm.get_axiom thy name)) of |
558 NONE => defs |
559 NONE => defs |
559 | SOME (s, (T, (args, rhs))) => Symtab.update |
560 | SOME (s, (T, (args, rhs))) => Symtab.curried_update |
560 ((s, (T, (thyname, split_last (rename_terms (args @ [rhs])))) :: |
561 (s, (T, (thyname, split_last (rename_terms (args @ [rhs])))) :: |
561 if_none (Symtab.lookup (defs, s)) []), defs))) |
562 if_none (Symtab.curried_lookup defs s) []) defs)) |
562 in |
563 in |
563 foldl (fn ((thyname, axms), defs) => |
564 foldl (fn ((thyname, axms), defs) => |
564 Symtab.foldl (add_def thyname) (defs, axms)) Symtab.empty axmss |
565 Symtab.foldl (add_def thyname) (defs, axms)) Symtab.empty axmss |
565 end; |
566 end; |
566 |
567 |
567 fun get_defn thy defs s T = (case Symtab.lookup (defs, s) of |
568 fun get_defn thy defs s T = (case Symtab.curried_lookup defs s of |
568 NONE => NONE |
569 NONE => NONE |
569 | SOME ds => |
570 | SOME ds => |
570 let val i = find_index (is_instance thy T o fst) ds |
571 let val i = find_index (is_instance thy T o fst) ds |
571 in if i >= 0 then |
572 in if i >= 0 then |
572 SOME (List.nth (ds, i), if length ds = 1 then NONE else SOME i) |
573 SOME (List.nth (ds, i), if length ds = 1 then NONE else SOME i) |
826 val gr = new_node ("<Top>", (NONE, module, "")) |
827 val gr = new_node ("<Top>", (NONE, module, "")) |
827 (foldl (fn ((gr, (tab1, tab2)), (gr', (tab1', tab2'))) => |
828 (foldl (fn ((gr, (tab1, tab2)), (gr', (tab1', tab2'))) => |
828 (Graph.merge (fn ((_, module, _), (_, module', _)) => |
829 (Graph.merge (fn ((_, module, _), (_, module', _)) => |
829 module = module') (gr, gr'), |
830 module = module') (gr, gr'), |
830 (merge_nametabs (tab1, tab1'), merge_nametabs (tab2, tab2')))) emptygr |
831 (merge_nametabs (tab1, tab1'), merge_nametabs (tab2, tab2')))) emptygr |
831 (map (fn s => case Symtab.lookup (graphs, s) of |
832 (map (fn s => case Symtab.curried_lookup graphs s of |
832 NONE => error ("Undefined code module: " ^ s) |
833 NONE => error ("Undefined code module: " ^ s) |
833 | SOME gr => gr) modules)) |
834 | SOME gr => gr) modules)) |
834 handle Graph.DUPS ks => error ("Duplicate code for " ^ commas ks); |
835 handle Graph.DUPS ks => error ("Duplicate code for " ^ commas ks); |
835 fun expand (t as Abs _) = t |
836 fun expand (t as Abs _) = t |
836 | expand t = (case fastype_of t of |
837 | expand t = (case fastype_of t of |
1053 (Path.append (Path.unpack fname) (Path.basic (name ^ ".ML"))) s) |
1054 (Path.append (Path.unpack fname) (Path.basic (name ^ ".ML"))) s) |
1054 (("ROOT", implode (map (fn (name, _) => |
1055 (("ROOT", implode (map (fn (name, _) => |
1055 "use \"" ^ name ^ ".ML\";\n") code)) :: code) |
1056 "use \"" ^ name ^ ".ML\";\n") code)) :: code) |
1056 else File.write (Path.unpack fname) (snd (hd code))); |
1057 else File.write (Path.unpack fname) (snd (hd code))); |
1057 if lib then thy |
1058 if lib then thy |
1058 else map_modules (fn graphs => |
1059 else map_modules (Symtab.curried_update (module, gr)) thy) |
1059 Symtab.update ((module, gr), graphs)) thy) |
|
1060 end)); |
1060 end)); |
1061 |
1061 |
1062 val code_libraryP = |
1062 val code_libraryP = |
1063 OuterSyntax.command "code_library" |
1063 OuterSyntax.command "code_library" |
1064 "generates code for terms (one structure for each theory)" K.thy_decl |
1064 "generates code for terms (one structure for each theory)" K.thy_decl |