62 val rename_term: term -> term |
62 val rename_term: term -> term |
63 val new_names: term -> string list -> string list |
63 val new_names: term -> string list -> string list |
64 val new_name: term -> string -> string |
64 val new_name: term -> string -> string |
65 val if_library: 'a -> 'a -> 'a |
65 val if_library: 'a -> 'a -> 'a |
66 val get_defn: theory -> deftab -> string -> typ -> |
66 val get_defn: theory -> deftab -> string -> typ -> |
67 ((typ * (string * (term list * term))) * int option) option |
67 ((typ * (string * thm)) * int option) option |
68 val is_instance: typ -> typ -> bool |
68 val is_instance: typ -> typ -> bool |
69 val parens: Pretty.T -> Pretty.T |
69 val parens: Pretty.T -> Pretty.T |
70 val mk_app: bool -> Pretty.T -> Pretty.T list -> Pretty.T |
70 val mk_app: bool -> Pretty.T -> Pretty.T list -> Pretty.T |
71 val mk_tuple: Pretty.T list -> Pretty.T |
71 val mk_tuple: Pretty.T list -> Pretty.T |
72 val mk_let: (Pretty.T * Pretty.T) list -> Pretty.T -> Pretty.T |
72 val mk_let: (Pretty.T * Pretty.T) list -> Pretty.T -> Pretty.T |
488 s = s' andalso is_instance T T') (#consts (CodegenData.get thy))); |
487 s = s' andalso is_instance T T') (#consts (CodegenData.get thy))); |
489 |
488 |
490 fun get_aux_code xs = map_filter (fn (m, code) => |
489 fun get_aux_code xs = map_filter (fn (m, code) => |
491 if m = "" orelse member (op =) (!mode) m then SOME code else NONE) xs; |
490 if m = "" orelse member (op =) (!mode) m then SOME code else NONE) xs; |
492 |
491 |
|
492 fun dest_prim_def t = |
|
493 let |
|
494 val (lhs, rhs) = Logic.dest_equals t; |
|
495 val (c, args) = strip_comb lhs; |
|
496 val (s, T) = dest_Const c |
|
497 in if forall is_Var args then SOME (s, (T, (args, rhs))) else NONE |
|
498 end handle TERM _ => NONE; |
|
499 |
493 fun mk_deftab thy = |
500 fun mk_deftab thy = |
494 let |
501 let |
495 val axmss = map (fn thy' => (Context.theory_name thy', Theory.axiom_table thy')) |
502 val axmss = map (fn thy' => (Context.theory_name thy', Theory.axiom_table thy')) |
496 (thy :: Theory.ancestors_of thy); |
503 (thy :: Theory.ancestors_of thy); |
497 fun prep_def def = (case preprocess thy [def] of |
504 fun prep_def def = (case preprocess thy [def] of |
498 [def'] => prop_of def' | _ => error "mk_deftab: bad preprocessor"); |
505 [def'] => prop_of def' | _ => error "mk_deftab: bad preprocessor"); |
499 fun dest t = |
506 fun add_def thyname (name, t) = (case dest_prim_def t of |
500 let |
|
501 val (lhs, rhs) = Logic.dest_equals t; |
|
502 val (c, args) = strip_comb lhs; |
|
503 val (s, T) = dest_Const c |
|
504 in if forall is_Var args then SOME (s, (T, (args, rhs))) else NONE |
|
505 end handle TERM _ => NONE; |
|
506 fun add_def thyname (name, t) = (case dest t of |
|
507 NONE => I |
507 NONE => I |
508 | SOME _ => (case dest (prep_def (Thm.axiom thy name)) of |
508 | SOME (s, (T, _)) => Symtab.map_default (s, []) |
509 NONE => I |
509 (cons (T, (thyname, Thm.axiom thy name)))); |
510 | SOME (s, (T, (args, rhs))) => Symtab.map_default (s, []) |
|
511 (cons (T, (thyname, split_last (rename_terms (args @ [rhs]))))))) |
|
512 in |
510 in |
513 fold (fn (thyname, axms) => Symtab.fold (add_def thyname) axms) axmss Symtab.empty |
511 fold (fn (thyname, axms) => Symtab.fold (add_def thyname) axms) axmss Symtab.empty |
|
512 end; |
|
513 |
|
514 fun prep_prim_def thy thm = |
|
515 let |
|
516 val prop = case preprocess thy [thm] |
|
517 of [thm'] => Thm.prop_of thm' |
|
518 | _ => error "mk_deftab: bad preprocessor" |
|
519 in ((Option.map o apsnd o apsnd) |
|
520 (fn (args, rhs) => split_last (rename_terms (args @ [rhs]))) o dest_prim_def) prop |
514 end; |
521 end; |
515 |
522 |
516 fun get_defn thy defs s T = (case Symtab.lookup defs s of |
523 fun get_defn thy defs s T = (case Symtab.lookup defs s of |
517 NONE => NONE |
524 NONE => NONE |
518 | SOME ds => |
525 | SOME ds => |
519 let val i = find_index (is_instance T o fst) ds |
526 let val i = find_index (is_instance T o fst) ds |
520 in if i >= 0 then |
527 in if i >= 0 then |
521 SOME (List.nth (ds, i), if length ds = 1 then NONE else SOME i) |
528 SOME (nth ds i, if length ds = 1 then NONE else SOME i) |
522 else NONE |
529 else NONE |
523 end); |
530 end); |
524 |
531 |
525 |
532 |
526 (**** invoke suitable code generator for term / type ****) |
533 (**** invoke suitable code generator for term / type ****) |
653 (p module'', add_edge (node_id, dep) gr4)) |
660 (p module'', add_edge (node_id, dep) gr4)) |
654 end |
661 end |
655 end |
662 end |
656 | NONE => (case get_defn thy defs s T of |
663 | NONE => (case get_defn thy defs s T of |
657 NONE => NONE |
664 NONE => NONE |
658 | SOME ((U, (thyname, (args, rhs))), k) => |
665 | SOME ((U, (thyname, thm)), k) => (case prep_prim_def thy thm |
659 let |
666 of SOME (_, (_, (args, rhs))) => let |
660 val module' = if_library thyname module; |
667 val module' = if_library thyname module; |
661 val suffix = (case k of NONE => "" | SOME i => " def" ^ string_of_int i); |
668 val suffix = (case k of NONE => "" | SOME i => " def" ^ string_of_int i); |
662 val node_id = s ^ suffix; |
669 val node_id = s ^ suffix; |
663 val ((ps, def_id), gr') = gr |> codegens true ts |
670 val ((ps, def_id), gr') = gr |> codegens true ts |
664 ||>> mk_const_id module' (s ^ suffix); |
671 ||>> mk_const_id module' (s ^ suffix); |
684 [str ("val " ^ snd def_id ^ " :"), ty] |
691 [str ("val " ^ snd def_id ^ " :"), ty] |
685 else str ("fun " ^ snd def_id) :: xs) @ |
692 else str ("fun " ^ snd def_id) :: xs) @ |
686 [str " =", Pretty.brk 1, p', str ";"])) ^ "\n\n")) gr4) |
693 [str " =", Pretty.brk 1, p', str ";"])) ^ "\n\n")) gr4) |
687 end |
694 end |
688 | SOME _ => (p, add_edge (node_id, dep) gr')) |
695 | SOME _ => (p, add_edge (node_id, dep) gr')) |
689 end)) |
696 end |
|
697 | NONE => NONE))) |
690 |
698 |
691 | Abs _ => |
699 | Abs _ => |
692 let |
700 let |
693 val (bs, Ts) = ListPair.unzip (strip_abs_vars u); |
701 val (bs, Ts) = ListPair.unzip (strip_abs_vars u); |
694 val t = strip_abs_body u |
702 val t = strip_abs_body u |