| Sat, 24 Oct 2009 16:55:42 +0200 |
bulwahn |
modularized the compilation in the predicate compiler
|
file |
diff |
annotate
|
| Sat, 24 Oct 2009 16:55:42 +0200 |
bulwahn |
modifying the depth-limited compilation to be sound, but now throws an error undefined in case of hitting the depth limit in an negative context; cleaning up the examples
|
file |
diff |
annotate
|
| Sat, 24 Oct 2009 16:55:42 +0200 |
bulwahn |
cleaning the signature of the predicate compiler core; renaming signature and structures to uniform long names
|
file |
diff |
annotate
|
| Sat, 24 Oct 2009 16:55:42 +0200 |
bulwahn |
added skip_proof option; playing with compilation of depth-limited predicates
|
file |
diff |
annotate
|
| Sat, 24 Oct 2009 16:55:42 +0200 |
bulwahn |
reinvestigating the compilation of the random computation in the predicate compiler
|
file |
diff |
annotate
|
| Sat, 24 Oct 2009 16:55:42 +0200 |
bulwahn |
added option to generate random values to values command in the predicate compiler
|
file |
diff |
annotate
|
| Sat, 24 Oct 2009 16:55:42 +0200 |
bulwahn |
commented out the random generator compilation in the example file
|
file |
diff |
annotate
|
| Sat, 24 Oct 2009 16:55:42 +0200 |
bulwahn |
changed import_intros to handle parameters differently; changed handling of higher-order function compilation; reverted MicroJava change; tuned
|
file |
diff |
annotate
|
| Sat, 24 Oct 2009 16:55:42 +0200 |
bulwahn |
further cleaning up
|
file |
diff |
annotate
|
| Sat, 24 Oct 2009 16:55:42 +0200 |
bulwahn |
importing of polymorphic introduction rules with different schematic variable names
|
file |
diff |
annotate
|
| Sat, 24 Oct 2009 16:55:42 +0200 |
bulwahn |
continued cleaning up; moved tuple expanding to core
|
file |
diff |
annotate
|
| Sat, 24 Oct 2009 16:55:42 +0200 |
bulwahn |
cleaned up debugging messages; added options to code_pred command
|
file |
diff |
annotate
|
| Sat, 24 Oct 2009 16:55:42 +0200 |
bulwahn |
cleaned up
|
file |
diff |
annotate
|
| Sat, 24 Oct 2009 16:55:42 +0200 |
bulwahn |
added theory with alternative definitions for the predicate compiler; cleaned up examples
|
file |
diff |
annotate
|
| Sat, 24 Oct 2009 16:55:42 +0200 |
bulwahn |
higher-order arguments in different rules are fixed to one name in the predicate compiler
|
file |
diff |
annotate
|
| Sat, 24 Oct 2009 16:55:42 +0200 |
bulwahn |
changed importing introduction rules to fix the same type variables in all introduction rules; improved mode analysis for partially applied relations; added test case; tuned
|
file |
diff |
annotate
|
| Sat, 24 Oct 2009 16:55:42 +0200 |
bulwahn |
added further examples; added mode to code_pred command; tuned; some temporary things in Predicate_Compile_ex
|
file |
diff |
annotate
|
| Sat, 24 Oct 2009 16:55:42 +0200 |
bulwahn |
processing of tuples in introduction rules
|
file |
diff |
annotate
|
| Sat, 24 Oct 2009 16:55:42 +0200 |
bulwahn |
added a few tricky examples with tuples; added alternative introduction rules for some constants; corrected mode analysis with negation; improved fetching of definitions
|
file |
diff |
annotate
|
| Sat, 24 Oct 2009 16:55:42 +0200 |
bulwahn |
developing an executable the operator
|
file |
diff |
annotate
|
| Sat, 24 Oct 2009 16:55:42 +0200 |
bulwahn |
added test for higher-order function inductification; added debug messages
|
file |
diff |
annotate
|
| Sat, 24 Oct 2009 16:55:35 +0200 |
bulwahn |
added tupled versions of examples for the predicate compiler
|
file |
diff |
annotate
|
| Sat, 24 Oct 2009 16:54:32 +0200 |
bulwahn |
moved meta_fun_cong lemma into ML-file; tuned
|
file |
diff |
annotate
|
| Wed, 23 Sep 2009 16:20:13 +0200 |
bulwahn |
replaced sorry by oops; removed old debug functions in predicate compiler
|
file |
diff |
annotate
|
| Wed, 23 Sep 2009 16:20:13 +0200 |
bulwahn |
added first version of quickcheck based on the predicate compiler; added a few quickcheck examples
|
file |
diff |
annotate
|
| Wed, 23 Sep 2009 16:20:12 +0200 |
bulwahn |
added a new example for the predicate compiler
|
file |
diff |
annotate
|
| Wed, 23 Sep 2009 16:20:12 +0200 |
bulwahn |
added context free grammar example; removed dead code; adapted to work without quick and dirty mode; fixed typo
|
file |
diff |
annotate
|
| Wed, 23 Sep 2009 16:20:12 +0200 |
bulwahn |
added first prototype of the extended predicate compiler
|
file |
diff |
annotate
|
| Wed, 23 Sep 2009 16:20:12 +0200 |
bulwahn |
extending predicate compiler and proof procedure to support tuples; testing predicate wirh HOL-MicroJava semantics
|
file |
diff |
annotate
|
| Tue, 15 Sep 2009 15:22:15 +0200 |
haftmann |
added singleton example
|
file |
diff |
annotate
|
| Thu, 27 Aug 2009 18:45:39 +0200 |
nipkow |
New example: IMP
|
file |
diff |
annotate
|
| Wed, 26 Aug 2009 16:13:19 +0200 |
nipkow |
new interval lemma
|
file |
diff |
annotate
|
| Mon, 10 Aug 2009 13:34:50 +0200 |
haftmann |
properly merged
|
file |
diff |
annotate
|
| Mon, 10 Aug 2009 10:25:00 +0200 |
haftmann |
merged
|
file |
diff |
annotate
|
| Thu, 30 Jul 2009 13:52:18 +0200 |
haftmann |
cleaned up
|
file |
diff |
annotate
|
| Tue, 04 Aug 2009 08:34:56 +0200 |
bulwahn |
improved use of context with cases rule in predicate compiler; predicate compiler based on Main for faster debugging
|
file |
diff |
annotate
|
| Tue, 04 Aug 2009 08:34:56 +0200 |
bulwahn |
commented rpred compilation; tuned
|
file |
diff |
annotate
|
| Tue, 04 Aug 2009 08:34:56 +0200 |
bulwahn |
added generator compilation of higher-order predicates; refined mode analysis for generators; some tuning
|
file |
diff |
annotate
|
| Tue, 04 Aug 2009 08:34:56 +0200 |
bulwahn |
changed resolving depending predicates and fetching in the predicate compiler
|
file |
diff |
annotate
|
| Tue, 04 Aug 2009 08:34:56 +0200 |
bulwahn |
extended mode inference by adding generators; adopted compilation; added some functions for constructing term closures
|
file |
diff |
annotate
|
| Tue, 30 Jun 2009 15:58:12 +0200 |
bulwahn |
commented trancl example; added debug message
|
file |
diff |
annotate
|
| Mon, 29 Jun 2009 12:33:58 +0200 |
bulwahn |
added diagnostic printing; changed proof for parameters; moved code
|
file |
diff |
annotate
|
| Fri, 12 Jun 2009 18:33:58 +0200 |
bulwahn |
added cases to code_pred command
|
file |
diff |
annotate
|
| Thu, 11 Jun 2009 22:04:23 +0200 |
bulwahn |
masking proof with a quick-and-dirty step
|
file |
diff |
annotate
|
| Thu, 11 Jun 2009 21:37:26 +0200 |
bulwahn |
improved infrastructure of predicate compiler for adding manual introduction rules
|
file |
diff |
annotate
|
| Thu, 11 Jun 2009 12:06:13 +0200 |
bulwahn |
making isatest happy; but misunderstanding remains
|
file |
diff |
annotate
|
| Wed, 10 Jun 2009 21:04:36 +0200 |
bulwahn |
code_pred command now also requires proofs for dependent predicates; changed handling of parameters in introrules of executable function
|
file |
diff |
annotate
|
| Tue, 09 Jun 2009 12:05:22 +0200 |
bulwahn |
refactoring the predicate compiler
|
file |
diff |
annotate
|
| Wed, 20 May 2009 22:24:07 +0200 |
haftmann |
experimental values command
|
file |
diff |
annotate
|
| Mon, 18 May 2009 15:45:42 +0200 |
haftmann |
added example on ML level
|
file |
diff |
annotate
|
| Tue, 12 May 2009 21:17:47 +0200 |
haftmann |
split Predicate_Compile examples into separate theory
|
file |
diff |
annotate
| base
|