62 val new_names: term -> string list -> string list |
62 val new_names: term -> string list -> string list |
63 val new_name: term -> string -> string |
63 val new_name: term -> string -> string |
64 val if_library: 'a -> 'a -> 'a |
64 val if_library: 'a -> 'a -> 'a |
65 val get_defn: theory -> deftab -> string -> typ -> |
65 val get_defn: theory -> deftab -> string -> typ -> |
66 ((typ * (string * (term list * term))) * int option) option |
66 ((typ * (string * (term list * term))) * int option) option |
67 val is_instance: theory -> typ -> typ -> bool |
67 val is_instance: typ -> typ -> bool |
68 val parens: Pretty.T -> Pretty.T |
68 val parens: Pretty.T -> Pretty.T |
69 val mk_app: bool -> Pretty.T -> Pretty.T list -> Pretty.T |
69 val mk_app: bool -> Pretty.T -> Pretty.T list -> Pretty.T |
70 val eta_expand: term -> term list -> int -> term |
70 val eta_expand: term -> term list -> int -> term |
71 val strip_tname: string -> string |
71 val strip_tname: string -> string |
72 val mk_type: bool -> typ -> Pretty.T |
72 val mk_type: bool -> typ -> Pretty.T |
528 val rename_term = hd o rename_terms o single; |
528 val rename_term = hd o rename_terms o single; |
529 |
529 |
530 |
530 |
531 (**** retrieve definition of constant ****) |
531 (**** retrieve definition of constant ****) |
532 |
532 |
533 fun is_instance thy T1 T2 = |
533 fun is_instance T1 T2 = |
534 Sign.typ_instance thy (T1, Logic.legacy_varifyT T2); |
534 Type.raw_instance (T1, Logic.legacy_varifyT T2); |
535 |
535 |
536 fun get_assoc_code thy (s, T) = Option.map snd (find_first (fn ((s', T'), _) => |
536 fun get_assoc_code thy (s, T) = Option.map snd (find_first (fn ((s', T'), _) => |
537 s = s' andalso is_instance thy T T') (#consts (CodegenData.get thy))); |
537 s = s' andalso is_instance T T') (#consts (CodegenData.get thy))); |
538 |
538 |
539 fun get_aux_code xs = map_filter (fn (m, code) => |
539 fun get_aux_code xs = map_filter (fn (m, code) => |
540 if m = "" orelse member (op =) (!mode) m then SOME code else NONE) xs; |
540 if m = "" orelse member (op =) (!mode) m then SOME code else NONE) xs; |
541 |
541 |
542 fun mk_deftab thy = |
542 fun mk_deftab thy = |
552 val (s, T) = dest_Const c |
552 val (s, T) = dest_Const c |
553 in if forall is_Var args then SOME (s, (T, (args, rhs))) else NONE |
553 in if forall is_Var args then SOME (s, (T, (args, rhs))) else NONE |
554 end handle TERM _ => NONE; |
554 end handle TERM _ => NONE; |
555 fun add_def thyname (name, t) = (case dest t of |
555 fun add_def thyname (name, t) = (case dest t of |
556 NONE => I |
556 NONE => I |
557 | SOME _ => (case dest (prep_def (Thm.get_axiom thy name)) of |
557 | SOME _ => (case dest (prep_def (Thm.get_axiom_i thy name)) of |
558 NONE => I |
558 NONE => I |
559 | SOME (s, (T, (args, rhs))) => Symtab.map_default (s, []) |
559 | SOME (s, (T, (args, rhs))) => Symtab.map_default (s, []) |
560 (cons (T, (thyname, split_last (rename_terms (args @ [rhs]))))))) |
560 (cons (T, (thyname, split_last (rename_terms (args @ [rhs]))))))) |
561 in |
561 in |
562 fold (fn (thyname, axms) => Symtab.fold (add_def thyname) axms) axmss Symtab.empty |
562 fold (fn (thyname, axms) => Symtab.fold (add_def thyname) axms) axmss Symtab.empty |
563 end; |
563 end; |
564 |
564 |
565 fun get_defn thy defs s T = (case Symtab.lookup defs s of |
565 fun get_defn thy defs s T = (case Symtab.lookup defs s of |
566 NONE => NONE |
566 NONE => NONE |
567 | SOME ds => |
567 | SOME ds => |
568 let val i = find_index (is_instance thy T o fst) ds |
568 let val i = find_index (is_instance T o fst) ds |
569 in if i >= 0 then |
569 in if i >= 0 then |
570 SOME (List.nth (ds, i), if length ds = 1 then NONE else SOME i) |
570 SOME (List.nth (ds, i), if length ds = 1 then NONE else SOME i) |
571 else NONE |
571 else NONE |
572 end); |
572 end); |
573 |
573 |