src/HOL/Tools/Metis/metis_translate.ML
Tue, 15 Nov 2011 22:13:39 +0100 blanchet disable debugging output
Tue, 15 Nov 2011 22:13:39 +0100 blanchet started implementing lambda-lifting in Metis
Thu, 22 Sep 2011 16:30:47 +0200 blanchet drop partial monomorphic instances in Metis, like in Sledgehammer
Thu, 22 Sep 2011 16:30:47 +0200 blanchet better type reconstruction -- prevents ill-instantiations in proof replay
Wed, 07 Sep 2011 13:50:16 +0200 blanchet tuning
Wed, 07 Sep 2011 09:10:41 +0200 blanchet rationalize uniform encodings
Thu, 25 Aug 2011 14:25:07 +0200 blanchet avoid using ":" for anything but systematic type tag annotations, because Hurd's Metis gives it that special semantics
Mon, 22 Aug 2011 15:02:45 +0200 blanchet change Metis's default settings if type information axioms are generated
Mon, 22 Aug 2011 15:02:45 +0200 blanchet prefer the lighter, slightly unsound monotonicity-based encodings for Metis
Mon, 22 Aug 2011 15:02:45 +0200 blanchet cleaner handling of polymorphic monotonicity inference
Mon, 22 Aug 2011 15:02:45 +0200 blanchet started cleaning up polymorphic monotonicity-based encodings, based on discussions with Nick Smallbone
Mon, 22 Aug 2011 15:02:45 +0200 blanchet added option to control soundness of encodings more precisely, for evaluation purposes
Tue, 09 Aug 2011 09:05:22 +0200 blanchet move lambda-lifting code to ATP encoding, so it can be used by Metis
Tue, 26 Jul 2011 14:53:00 +0200 blanchet tuning -- remove useless function (at this point combinators are already in)
Sun, 17 Jul 2011 14:12:45 +0200 blanchet ensure that the lambda translation procedure is called only once with all the facts, which is necessary for soundness of lambda-lifting (freshness of new names)
Sun, 17 Jul 2011 14:11:35 +0200 blanchet pass kind to lambda-translation function
Sun, 17 Jul 2011 14:11:34 +0200 blanchet move more lambda-handling logic to Sledgehammer, from ATP module, for formal dependency reasons
Thu, 14 Jul 2011 16:50:05 +0200 blanchet move lambda translation option from ATP to Sledgehammer, to avoid accidentally breaking Metis (its reconstruction code can only deal with combinators)
Thu, 14 Jul 2011 15:14:38 +0200 blanchet fix subtle type inference bug in Metis -- different occurrences of the same Skolem might need to be typed differently, using paramify_vars overconstraints the typing problem
Fri, 01 Jul 2011 15:53:38 +0200 blanchet renamed "type_sys" to "type_enc", which is more accurate
Mon, 27 Jun 2011 14:56:28 +0200 blanchet added "sound" option to force Sledgehammer to be pedantically sound
Tue, 21 Jun 2011 17:17:39 +0200 blanchet remove historical bloat -- another benefit of merging Metis's and Sledgehammer's translations
Thu, 09 Jun 2011 00:16:28 +0200 blanchet cleaner fact freshening, which also works in corner cases, e.g. if two backquoted facts have the same name (but have different variable indices)
Wed, 08 Jun 2011 16:20:19 +0200 blanchet pass Metis facts and negated conjecture as facts, with (almost) correctly set localities, so that the correct encoding is used for nonmonotonic occurrences of infinite types
Wed, 08 Jun 2011 08:47:43 +0200 blanchet removed yet another hack in "make_metis" script -- respect opacity of "Metis_Name.name"
Wed, 08 Jun 2011 08:47:43 +0200 blanchet killed "explicit_apply" option in Sledgehammer -- the "smart" default is about as lightweight as "false" and just as complete as "true"
Tue, 07 Jun 2011 14:17:35 +0200 blanchet more suitable implementation of "schematic_consts_of" for monomorphizer, for ATPs
Tue, 07 Jun 2011 10:46:09 +0200 blanchet removed "verbose" option -- there won't be any verbosity in there, according to Sascha (yeah)
Tue, 07 Jun 2011 10:43:18 +0200 blanchet nicely thread monomorphism verbosity in Metis and Sledgehammer
Tue, 07 Jun 2011 07:06:24 +0200 blanchet renamed ML function
Mon, 06 Jun 2011 20:56:06 +0200 blanchet Metis code cleanup
Mon, 06 Jun 2011 20:36:36 +0200 blanchet enable new Metis
Mon, 06 Jun 2011 20:36:35 +0200 blanchet more preparations towards hijacking Metis
Mon, 06 Jun 2011 20:36:35 +0200 blanchet make "metisX"'s default more like old "metis"
Mon, 06 Jun 2011 20:36:35 +0200 blanchet fixed type helper indices in new Metis
Mon, 06 Jun 2011 20:36:35 +0200 blanchet improved ATP clausifier so it can deal with "x => (y <=> z)"
Mon, 06 Jun 2011 20:36:35 +0200 blanchet don't translate new Skolemizer assumptions in new Metis
Mon, 06 Jun 2011 20:36:35 +0200 blanchet tuning
Mon, 06 Jun 2011 20:36:35 +0200 blanchet conceal old Skolems in new Metis
Mon, 06 Jun 2011 20:36:35 +0200 blanchet properly locate helpers whose constants have several entries in the helper table
Mon, 06 Jun 2011 20:36:35 +0200 blanchet skip "hBOOL" in new Metis path finder
Mon, 06 Jun 2011 20:36:35 +0200 blanchet don't pass "~ " to new Metis
Mon, 06 Jun 2011 20:36:34 +0200 blanchet clean up unnecessary machinery -- helpers work also with monomorphic type encodings
Mon, 06 Jun 2011 20:36:34 +0200 blanchet added support for helpers in new Metis, so far only for polymorphic type encodings
Wed, 01 Jun 2011 10:29:43 +0200 blanchet ensured monomorphized facts have normalized zero var indexes, so that "find_var" doesn't fail later on
Wed, 01 Jun 2011 10:29:43 +0200 blanchet implemented missing hAPP and ti cases of new path finder
Wed, 01 Jun 2011 10:29:43 +0200 blanchet support lightweight tags in new Metis
Wed, 01 Jun 2011 10:29:43 +0200 blanchet tuned names
Wed, 01 Jun 2011 10:29:43 +0200 blanchet distinguish different kinds of typing informations in the fact name
Tue, 31 May 2011 16:38:36 +0200 blanchet monomorphize in the new Metis if the type system calls for it
Tue, 31 May 2011 16:38:36 +0200 blanchet fixed new path finder for type information tag
Tue, 31 May 2011 16:38:36 +0200 blanchet use ":" for type information (looks good in Metis's output) and handle it in new path finder
Tue, 31 May 2011 16:38:36 +0200 blanchet tuned name
Tue, 31 May 2011 16:38:36 +0200 blanchet tuned name
Tue, 31 May 2011 16:38:36 +0200 blanchet parse optional type system specification
Tue, 31 May 2011 16:38:36 +0200 blanchet proper handling of type variable classes in new Metis
Tue, 31 May 2011 16:38:36 +0200 blanchet don't preprocess twice
Tue, 31 May 2011 16:38:36 +0200 blanchet more work on new Metis
Tue, 31 May 2011 16:38:36 +0200 blanchet tuning
Tue, 31 May 2011 16:38:36 +0200 blanchet more work on new metis that exploits the powerful new type encodings
less more (0) -60 tip