#
1539a252 |
|
09-Mar-2020 |
wenzelm <none@none> |
tuned signature;
|
#
3b657802 |
|
17-Feb-2020 |
wenzelm <none@none> |
proper sort constraints for strip_shyps, for sort relations used in minimization;
|
#
896ec975 |
|
26-May-2018 |
wenzelm <none@none> |
export sort algebra;
|
#
56f8495e |
|
08-Mar-2016 |
haftmann <none@none> |
provide explicit hint concering uniqueness of derivation
|
#
763a1fb4 |
|
25-Sep-2015 |
wenzelm <none@none> |
tuned;
|
#
6033868f |
|
25-Sep-2015 |
wenzelm <none@none> |
tuned signature: eliminated pointless type Context.pretty;
|
#
b0e9e6ce |
|
16-Jul-2012 |
wenzelm <none@none> |
more direct Sorts.has_instance; tuned Sorts.mg_domain;
|
#
551b966c |
|
18-Mar-2012 |
wenzelm <none@none> |
maintain generic context naming in structure Name_Space (NB: empty = default_naming, init = local_naming); more explicit Context.generic for Name_Space.declare/define and derivatives (NB: naming changed after Proof_Context.init_global); prefer Context.pretty in low-level operations of structure Sorts/Type (defer full Syntax.init_pretty until error output); simplified signatures;
|
#
9f564a6a |
|
23-Feb-2012 |
wenzelm <none@none> |
clarified Graph.restrict (formerly Graph.subgraph) based on public graph operations;
|
#
5536b323 |
|
20-Nov-2011 |
wenzelm <none@none> |
clarified certify vs. sharing;
|
#
d049bd7b |
|
20-Aug-2011 |
wenzelm <none@none> |
refined Graph implementation: more abstract/scalable Graph.Keys instead of plain lists -- order of adjacency is now standardized wrt. Key.ord;
|
#
3eb59a2e |
|
13-Jul-2011 |
wenzelm <none@none> |
Table.lookup_key and Graph.get_entry allow to retrieve the original key, which is not necessarily identical to the given one; Sorts.certify_class: prefer the persistent name;
|
#
f53da0a1 |
|
18-Apr-2011 |
wenzelm <none@none> |
pass plain Proof.context for pretty printing;
|
#
3177e5c8 |
|
17-Apr-2011 |
wenzelm <none@none> |
simplified Sorts.class_error: plain Proof.context; tuned;
|
#
dbff82ee |
|
18-Apr-2011 |
wenzelm <none@none> |
simplified pretty printing context, which is only required for certain kernel operations; disentangled dependencies of structure Pretty;
|
#
86bc1118 |
|
24-Sep-2010 |
wenzelm <none@none> |
modernized structure Ord_List;
|
#
9e2201a3 |
|
01-Sep-2010 |
haftmann <none@none> |
replaced Table.map' by Table.map
|
#
b4ac0fdf |
|
01-Jun-2010 |
wenzelm <none@none> |
arities: no need to maintain original codomain (cf. f795c1164708) -- completion happens in axclass.ML; misc tuning;
|
#
7081aa46 |
|
27-Apr-2010 |
wenzelm <none@none> |
monotonic sort certification: sorts are no longer minimized at the kernel boundary, only when reading input from the end-user;
|
#
f9144b32 |
|
25-Apr-2010 |
wenzelm <none@none> |
replaced Sorts.rep_algebra by slightly more abstract selectors classes_of/arities_of;
|
#
d86b9424 |
|
11-Apr-2010 |
wenzelm <none@none> |
modernized datatype constructors;
|
#
06ae1e66 |
|
11-Apr-2010 |
wenzelm <none@none> |
of_sort_derivation: weaken bypasses derivation for identical sort -- accomodate proof terms by krauss/schropp, for example;
|
#
09e0b97c |
|
11-Apr-2010 |
wenzelm <none@none> |
tuned;
|
#
06b4848e |
|
11-Apr-2010 |
wenzelm <none@none> |
of_sort_derivation: pass-through full type information -- following the version by krauss/schropp;
|
#
cfd4dd69 |
|
26-Mar-2010 |
wenzelm <none@none> |
more efficient merge_algebra for important special cases -- tricky due to required completion if class algebra changes;
|
#
26716d38 |
|
25-Mar-2010 |
wenzelm <none@none> |
Sorts.of_sort_derivation: do not use slow Graph.irreducible_paths here, which not always needed (SUBTLE CHANGE IN SEMANTICS); officially export weaken as Sorts.classrel_derivation; tuned comments;
|
#
e3d0611a |
|
27-Feb-2010 |
wenzelm <none@none> |
modernized structure Term_Ord;
|
#
68478f6d |
|
20-Oct-2009 |
haftmann <none@none> |
replaced old_style infixes eq_set, subset, union, inter and variants by generic versions
|
#
0001a658 |
|
30-Sep-2009 |
wenzelm <none@none> |
removed dead code; Sorts.of_sort_derivation: removed unused pp;
|
#
51ddcad2 |
|
06-Jul-2009 |
wenzelm <none@none> |
witness_sorts: proper type witnesses for hyps, not invented "'hyp" variables;
|
#
121e82fb |
|
04-Mar-2009 |
blanchet <none@none> |
Merge.
|
#
03cabefa |
|
23-Feb-2009 |
haftmann <none@none> |
stripped classrels_of, instances_of
|
#
9b1624a4 |
|
22-Feb-2009 |
haftmann <none@none> |
handle NONE case in arity function properly
|
#
9d758fb7 |
|
22-Feb-2009 |
haftmann <none@none> |
subalgebra: drop arities if desired
|
#
8ebaa7ff |
|
18-Feb-2009 |
haftmann <none@none> |
sort instances wrt. to class hierarchy
|
#
e154e805 |
|
31-Dec-2008 |
wenzelm <none@none> |
moved term order operations to structure TermOrd (cf. Pure/term_ord.ML); tuned signature of structure Term;
|
#
969b8b39 |
|
30-Nov-2008 |
haftmann <none@none> |
more means for algebra projection
|
#
63e1cf16 |
|
22-Oct-2008 |
haftmann <none@none> |
added meet_sort_typ
|
#
5f476ac6 |
|
16-Oct-2008 |
wenzelm <none@none> |
added make, minimal_sorts;
|
#
d32a10d9 |
|
26-Sep-2008 |
wenzelm <none@none> |
added subset operation;
|
#
4ff1faf4 |
|
25-Sep-2008 |
wenzelm <none@none> |
explicit type OrdList.T;
|
#
f3d8b2ed |
|
11-Jul-2008 |
wenzelm <none@none> |
Sorts.weaken: abstract argument; tuned;
|
#
8dbd5fcb |
|
11-Jul-2008 |
haftmann <none@none> |
fixed layout
|
#
44817bf8 |
|
08-Jul-2008 |
haftmann <none@none> |
exported weaken combinator
|
#
56b6505c |
|
26-May-2008 |
haftmann <none@none> |
proper NoSubsort CLASS_ERROR
|
#
49a8b93a |
|
13-Apr-2008 |
wenzelm <none@none> |
removed unused minimal_classes; class_error: produce message only (formerly msg_class_error); tuned;
|
#
6a3c749e |
|
02-Apr-2008 |
haftmann <none@none> |
canonical meet_sort operation
|
#
855d6ae2 |
|
19-Mar-2008 |
haftmann <none@none> |
new class error case NoSubsort
|
#
e409919e |
|
26-Sep-2007 |
wenzelm <none@none> |
added minimize_sort, complete_sort;
|
#
5110e11c |
|
08-Jul-2007 |
wenzelm <none@none> |
replaced exception TableFun/GraphFun.DUPS by TableFun/GraphFun.DUP;
|
#
f34b7056 |
|
04-Jul-2007 |
wenzelm <none@none> |
sort_le: tuned eq case;
|
#
bae9892c |
|
03-Apr-2007 |
wenzelm <none@none> |
renamed of_sort_derivation record fields (avoid clash with Alice keywords);
|
#
921aa0c0 |
|
26-Feb-2007 |
wenzelm <none@none> |
removed obsolete eq_set;
|
#
12022caa |
|
26-Jan-2007 |
haftmann <none@none> |
exported interface for explicit error messages
|
#
9b6a860c |
|
25-Jan-2007 |
haftmann <none@none> |
added explicit query function for arities to subalgebra projection
|
#
aa4cac16 |
|
29-Dec-2006 |
wenzelm <none@none> |
classes: more direct way to achieve topological sorting; renamed classes to all_classes; added minimal_classes; renamed project to subalgebra, tuned;
|
#
69848c00 |
|
28-Dec-2006 |
haftmann <none@none> |
``classes`` now returns classes in topological order
|
#
7561ae60 |
|
18-Sep-2006 |
wenzelm <none@none> |
classes: maintain serial number;
|
#
7f08a740 |
|
04-Sep-2006 |
haftmann <none@none> |
proper project_sort
|
#
6520db80 |
|
01-Sep-2006 |
haftmann <none@none> |
project_algebra yields sort projector
|
#
9937031e |
|
17-Aug-2006 |
haftmann <none@none> |
added all_super_classes
|
#
be050e24 |
|
03-Jul-2006 |
wenzelm <none@none> |
project_algebra: norm_sort; tuned;
|
#
774d99a1 |
|
27-Jun-2006 |
haftmann <none@none> |
added class projection
|
#
833cda8e |
|
16-May-2006 |
wenzelm <none@none> |
abstract interfaces for type algebra; tuned;
|
#
fad69875 |
|
06-May-2006 |
wenzelm <none@none> |
tuned;
|
#
b3cb904b |
|
05-May-2006 |
wenzelm <none@none> |
added class_error and exception CLASS_ERROR (supercedes DOMAIN); clarified of_class_derivation; tuned witness_sorts;
|
#
f07448db |
|
01-May-2006 |
wenzelm <none@none> |
tuned;
|
#
764825a0 |
|
01-May-2006 |
wenzelm <none@none> |
added domain_error; added of_sort_derivation; tuned;
|
#
4e028643 |
|
01-May-2006 |
wenzelm <none@none> |
arities: maintain original codomain;
|
#
ee463f0d |
|
30-Apr-2006 |
wenzelm <none@none> |
moved certify_class/sort to type.ML; added operations to build sort algebras (from type.ML); tuned;
|
#
cf09f0e2 |
|
27-Apr-2006 |
wenzelm <none@none> |
tuned basic list operators (flat, maps, map_filter);
|
#
64f676be |
|
25-Apr-2006 |
wenzelm <none@none> |
added remove_sort;
|
#
7dd261c8 |
|
11-Apr-2006 |
wenzelm <none@none> |
removed superclasses (see sign.ML);
|
#
015764c5 |
|
09-Apr-2006 |
wenzelm <none@none> |
removed unused class_le_path, sort_less;
|
#
f16833ca |
|
06-Feb-2006 |
wenzelm <none@none> |
TableFun: renamed xxx_multi to xxx_list;
|
#
6b36083c |
|
16-Dec-2005 |
wenzelm <none@none> |
sort_distinct;
|
#
db589537 |
|
04-Oct-2005 |
wenzelm <none@none> |
minor tweaks for Poplog/ML;
|
#
45dec154 |
|
15-Sep-2005 |
wenzelm <none@none> |
TableFun/Symtab: curried lookup and update;
|
#
c968ef97 |
|
01-Sep-2005 |
wenzelm <none@none> |
curried_lookup/update;
|
#
2085d1ed |
|
29-Aug-2005 |
wenzelm <none@none> |
use AList operations;
|
#
f15c3e55 |
|
28-Aug-2005 |
haftmann <none@none> |
added superclasses, class_le_path
|
#
2989693d |
|
19-Jul-2005 |
wenzelm <none@none> |
tuned norm_sort, mg_domain;
|
#
a592d079 |
|
29-Jun-2005 |
wenzelm <none@none> |
removed obsolete eq_sort, mem_sort, subset_sort, eq_set_sort, ins_sort, union_sort, rems_sort; added efficient operations on ordered lists: eq_set, union, subtract, insert_sort/typ(s)/term(s);
|
#
19fac3d9 |
|
15-Jun-2005 |
haftmann <none@none> |
(undone experimental changes)
|
#
d6830efd |
|
15-Jun-2005 |
haftmann <none@none> |
subclassing done
|
#
eee46a1e |
|
02-Mar-2005 |
skalberg <none@none> |
Move towards standard functions.
|
#
3dffd254 |
|
13-Feb-2005 |
skalberg <none@none> |
Deleted Library.option type.
|
#
75e28697 |
|
21-Jun-2004 |
wenzelm <none@none> |
added certify_class/sort;
|
#
1f4db9f7 |
|
05-Jun-2004 |
wenzelm <none@none> |
tuned comments;
|
#
40c81668 |
|
29-May-2004 |
wenzelm <none@none> |
improved output; refer to Pretty.pp;
|
#
4aa55f84 |
|
21-May-2004 |
wenzelm <none@none> |
incorporate sort ops from term.ML; use Graph.T; misc cleanup;
|
#
115c7cea |
|
07-Jul-2000 |
wenzelm <none@none> |
inter_sort: keep normal!
|
#
12880449 |
|
29-Sep-1999 |
wenzelm <none@none> |
mg_domain: exception DOMAIN; proper witness_sorts; removed nonempty_sort;
|
#
8c14ea50 |
|
23-Jul-1999 |
wenzelm <none@none> |
replace assoc lists by Symtab.table;
|
#
ff898ab5 |
|
06-Oct-1997 |
wenzelm <none@none> |
now uses Syntax.simple_str_of_sort;
|
#
d054d3dd |
|
06-Aug-1997 |
wenzelm <none@none> |
added str_of_classrel;
|
#
0634c006 |
|
18-Apr-1997 |
wenzelm <none@none> |
removed least_sort; added of_sort;
|
#
1ef97499 |
|
16-Apr-1997 |
wenzelm <none@none> |
Type classes and sorts (isolated from type.ML).
|