equal
deleted
inserted
replaced
9 sig |
9 sig |
10 type T |
10 type T |
11 val eq_consts: T * T -> bool |
11 val eq_consts: T * T -> bool |
12 val change_base: bool -> T -> T |
12 val change_base: bool -> T -> T |
13 val change_ignore: T -> T |
13 val change_ignore: T -> T |
14 val retrieve_abbrevs: T -> string list -> term -> (term * term) list |
14 val revert_abbrevs: T -> string list -> (term * term) Item_Net.T list |
15 val dest: T -> |
15 val dest: T -> |
16 {const_space: Name_Space.T, |
16 {const_space: Name_Space.T, |
17 constants: (string * (typ * term option)) list, |
17 constants: (string * (typ * term option)) list, |
18 constraints: (string * typ) list} |
18 constraints: (string * typ) list} |
19 val get_const_name: T -> string -> string option |
19 val get_const_name: T -> string -> string option |
83 Item_Net.init (fn ((t, u), (t', u')) => t aconv t' andalso u aconv u') (single o #1); |
83 Item_Net.init (fn ((t, u), (t', u')) => t aconv t' andalso u aconv u') (single o #1); |
84 |
84 |
85 fun update_abbrevs mode abbrs = |
85 fun update_abbrevs mode abbrs = |
86 Symtab.map_default (mode, empty_abbrevs) (Item_Net.update abbrs); |
86 Symtab.map_default (mode, empty_abbrevs) (Item_Net.update abbrs); |
87 |
87 |
88 fun retrieve_abbrevs (Consts {rev_abbrevs, ...}) modes = |
88 fun revert_abbrevs (Consts {rev_abbrevs, ...}) modes = |
89 let val nets = map_filter (Symtab.lookup rev_abbrevs) modes in |
89 map_filter (Symtab.lookup rev_abbrevs) modes; |
90 fn t => |
|
91 let |
|
92 val retrieve = |
|
93 if Term.could_beta_eta_contract t |
|
94 then Item_Net.retrieve |
|
95 else Item_Net.retrieve_matching |
|
96 in maps (fn net => retrieve net t) nets end |
|
97 end; |
|
98 |
90 |
99 |
91 |
100 (* dest consts *) |
92 (* dest consts *) |
101 |
93 |
102 fun dest (Consts {decls, constraints, ...}) = |
94 fun dest (Consts {decls, constraints, ...}) = |