darcs-mirror-isa-launchbury.git
5 years agoDemand more in FutureAnalysisCarrier
Joachim Breitner [Fri, 19 Dec 2014 15:29:47 +0000 (15:29 +0000)]
Demand more in FutureAnalysisCarrier

5 years agoFix indentation
Joachim Breitner [Fri, 19 Dec 2014 13:57:59 +0000 (13:57 +0000)]
Fix indentation

5 years agoMore lemmas moved
Joachim Breitner [Fri, 19 Dec 2014 13:56:07 +0000 (13:56 +0000)]
More lemmas moved

5 years agoMake Tex more robust
Joachim Breitner [Fri, 19 Dec 2014 13:47:00 +0000 (13:47 +0000)]
Make Tex more robust

5 years agoLots of cleanup
Joachim Breitner [Fri, 19 Dec 2014 13:05:25 +0000 (13:05 +0000)]
Lots of cleanup

5 years agoSorry-Frei! (Fehlt noch: Nicht-rekursive Lets, und dann noch _?_:_)
Joachim Breitner [Wed, 17 Dec 2014 14:38:05 +0000 (14:38 +0000)]
Sorry-Frei! (Fehlt noch: Nicht-rekursive Lets, und dann noch _?_:_)

5 years agoMake CoCallAnalyis use Afix from ArityAnalysis
Joachim Breitner [Tue, 16 Dec 2014 14:39:36 +0000 (14:39 +0000)]
Make CoCallAnalyis use Afix from ArityAnalysis

5 years agoFix some sorries
Joachim Breitner [Tue, 16 Dec 2014 12:55:55 +0000 (12:55 +0000)]
Fix some sorries

5 years agoAfix does not have to take CoCallGraph into account
Joachim Breitner [Tue, 16 Dec 2014 12:38:55 +0000 (12:38 +0000)]
Afix does not have to take CoCallGraph into account

5 years agoedom_Afix
Joachim Breitner [Mon, 15 Dec 2014 16:05:25 +0000 (16:05 +0000)]
edom_Afix

5 years agoLooks like no special treatment for linear recursion is needed here
Joachim Breitner [Mon, 15 Dec 2014 14:30:05 +0000 (14:30 +0000)]
Looks like no special treatment for linear recursion is needed here

5 years agoccFTree_below_singleI, paths_withoutI
Joachim Breitner [Fri, 12 Dec 2014 16:33:08 +0000 (16:33 +0000)]
ccFTree_below_singleI, paths_withoutI

5 years agoLarge unsorted commit. Special casing for linear recursion started.
Joachim Breitner [Thu, 11 Dec 2014 13:19:54 +0000 (13:19 +0000)]
Large unsorted commit. Special casing for linear recursion started.

5 years agoAdd join_comm, join_assoc to simpset. Hopefully helpful stuff in CoCallCardinality
Joachim Breitner [Wed, 3 Dec 2014 16:21:20 +0000 (16:21 +0000)]
Add join_comm, join_assoc to simpset. Hopefully helpful stuff in CoCallCardinality

5 years agoAdjust CardinalityEtaExpand and FTreeCardinatly to annoying new parameter of substitute
Joachim Breitner [Mon, 1 Dec 2014 12:42:17 +0000 (12:42 +0000)]
Adjust CardinalityEtaExpand and FTreeCardinatly to annoying new parameter of substitute

5 years agoSchadensbegrenzung. substitute mit extra "thunks" Parameter
Joachim Breitner [Wed, 26 Nov 2014 16:07:51 +0000 (16:07 +0000)]
Schadensbegrenzung. substitute mit extra "thunks" Parameter

5 years agoTowards Let, but stuck: stubstitute needs to cater for sharing of the result!
Joachim Breitner [Wed, 26 Nov 2014 10:18:04 +0000 (10:18 +0000)]
Towards Let, but stuck: stubstitute needs to cater for sharing of the result!

5 years agoNon-Let-parts of CoCalls-to-ftree Conversation
Joachim Breitner [Tue, 25 Nov 2014 15:48:41 +0000 (15:48 +0000)]
Non-Let-parts of CoCalls-to-ftree Conversation

5 years agoCleanup
Joachim Breitner [Fri, 21 Nov 2014 14:58:59 +0000 (14:58 +0000)]
Cleanup

5 years agoFactor out AnalBinds
Joachim Breitner [Fri, 21 Nov 2014 12:39:58 +0000 (12:39 +0000)]
Factor out AnalBinds

5 years agoDisjointness lemmas in FTreeCardinality
Joachim Breitner [Fri, 21 Nov 2014 12:17:57 +0000 (12:17 +0000)]
Disjointness lemmas in FTreeCardinality

5 years agoContinuity of substitute, both
Joachim Breitner [Thu, 20 Nov 2014 15:25:17 +0000 (15:25 +0000)]
Continuity of substitute, both

5 years agoNice syntax for either
Joachim Breitner [Thu, 20 Nov 2014 14:35:02 +0000 (14:35 +0000)]
Nice syntax for either

5 years agoNice syntax for both
Joachim Breitner [Thu, 20 Nov 2014 14:30:16 +0000 (14:30 +0000)]
Nice syntax for both

5 years agoReorder lemmas in FTree
Joachim Breitner [Thu, 20 Nov 2014 13:45:05 +0000 (13:45 +0000)]
Reorder lemmas in FTree

5 years agoYay for force
Joachim Breitner [Wed, 19 Nov 2014 09:41:44 +0000 (09:41 +0000)]
Yay for force

5 years agoNew file List-Interleavings
Joachim Breitner [Wed, 19 Nov 2014 09:39:00 +0000 (09:39 +0000)]
New file List-Interleavings

5 years agoHuge proofs for ftree_restr_both and ftree_rest_substitute
Joachim Breitner [Tue, 18 Nov 2014 16:23:59 +0000 (16:23 +0000)]
Huge proofs for ftree_restr_both and ftree_rest_substitute

5 years agoPlan for CardinalityPrognosisCorrectLet
Joachim Breitner [Mon, 17 Nov 2014 15:55:47 +0000 (15:55 +0000)]
Plan for CardinalityPrognosisCorrectLet

5 years agoAvoid talking about substitute'
Joachim Breitner [Mon, 17 Nov 2014 15:26:40 +0000 (15:26 +0000)]
Avoid talking about substitute'

5 years agoCardinalityPrognosisCorrect fertig
Joachim Breitner [Mon, 17 Nov 2014 09:56:08 +0000 (09:56 +0000)]
CardinalityPrognosisCorrect fertig

5 years agoMore progress on variables rules in various variants
Joachim Breitner [Fri, 14 Nov 2014 15:00:57 +0000 (15:00 +0000)]
More progress on variables rules in various variants

5 years agoFrom ftree to cardinality
Joachim Breitner [Fri, 14 Nov 2014 11:35:56 +0000 (11:35 +0000)]
From ftree to cardinality

5 years agoStuff in FutureCardinality.thy
Joachim Breitner [Fri, 14 Nov 2014 11:35:43 +0000 (11:35 +0000)]
Stuff in FutureCardinality.thy

5 years agoLess assumptions passed to prognosis_Var
Joachim Breitner [Fri, 14 Nov 2014 11:35:09 +0000 (11:35 +0000)]
Less assumptions passed to prognosis_Var

5 years agoType of infinite trees as down-ward-closed sets of paths
Joachim Breitner [Fri, 14 Nov 2014 11:34:55 +0000 (11:34 +0000)]
Type of infinite trees as down-ward-closed sets of paths

5 years agoBridge from Cardinality Analysis to Prognosis based correctness
Joachim Breitner [Tue, 11 Nov 2014 12:15:21 +0000 (12:15 +0000)]
Bridge from Cardinality Analysis to Prognosis based correctness

5 years agoRemove unused Arity Correctness locales
Joachim Breitner [Mon, 10 Nov 2014 12:06:39 +0000 (12:06 +0000)]
Remove unused Arity Correctness locales

5 years agoUse FutureEtaExpand proof also in ArityEtaExpand proof
Joachim Breitner [Mon, 10 Nov 2014 09:42:59 +0000 (09:42 +0000)]
Use FutureEtaExpand proof also in ArityEtaExpand proof

5 years agoFound a sorry...
Joachim Breitner [Thu, 6 Nov 2014 15:54:13 +0000 (15:54 +0000)]
Found a sorry...

5 years agoAdding a trivial cardinality analysis to an arity analysis
Joachim Breitner [Thu, 6 Nov 2014 15:43:59 +0000 (15:43 +0000)]
Adding a trivial cardinality analysis to an arity analysis

5 years agos/fHeap/cHeap/g
Joachim Breitner [Thu, 6 Nov 2014 12:58:25 +0000 (12:58 +0000)]
s/fHeap/cHeap/g

5 years agoClean out FutureEtaExpand
Joachim Breitner [Thu, 6 Nov 2014 12:51:57 +0000 (12:51 +0000)]
Clean out FutureEtaExpand

5 years agoAll sorries moved to assumptions
Joachim Breitner [Wed, 5 Nov 2014 15:59:49 +0000 (15:59 +0000)]
All sorries moved to assumptions

5 years agoGet rid of aSummary
Joachim Breitner [Wed, 5 Nov 2014 15:24:56 +0000 (15:24 +0000)]
Get rid of aSummary

5 years agoRephrase stuff in terms of aSummary
Joachim Breitner [Wed, 5 Nov 2014 13:15:38 +0000 (13:15 +0000)]
Rephrase stuff in terms of aSummary

5 years agoMake aBinds nicer
Joachim Breitner [Wed, 5 Nov 2014 12:54:56 +0000 (12:54 +0000)]
Make aBinds nicer

5 years agoStuff...
Joachim Breitner [Wed, 5 Nov 2014 10:03:56 +0000 (10:03 +0000)]
Stuff...

5 years agoSimplify aHeap and fHeap
Joachim Breitner [Tue, 4 Nov 2014 15:32:43 +0000 (15:32 +0000)]
Simplify aHeap and fHeap

5 years agoMore stuff in FutureEtaExpand
Joachim Breitner [Tue, 4 Nov 2014 14:48:40 +0000 (14:48 +0000)]
More stuff in FutureEtaExpand

5 years agoThe frame for the proof for let
Joachim Breitner [Mon, 3 Nov 2014 16:16:18 +0000 (16:16 +0000)]
The frame for the proof for let

5 years agoMore work on that, but now stuck: Again information lost during thunk evaluation...
Joachim Breitner [Fri, 31 Oct 2014 15:30:52 +0000 (15:30 +0000)]
More work on that, but now stuck: Again information lost during thunk evaluation...

5 years agoProgress towards a correctness proof based on futures
Joachim Breitner [Fri, 31 Oct 2014 10:28:14 +0000 (10:28 +0000)]
Progress towards a correctness proof based on futures

5 years agoBeginnings of CallArityEtaExpand.thy
Joachim Breitner [Fri, 24 Oct 2014 08:51:04 +0000 (08:51 +0000)]
Beginnings of CallArityEtaExpand.thy

5 years agoSlightly more general AbstractTransform
Joachim Breitner [Fri, 24 Oct 2014 08:30:20 +0000 (08:30 +0000)]
Slightly more general AbstractTransform

5 years agoDefine ccExp
Joachim Breitner [Thu, 23 Oct 2014 14:41:25 +0000 (14:41 +0000)]
Define ccExp

5 years agoRahmem für die CC-Analyse
Joachim Breitner [Wed, 22 Oct 2014 15:24:06 +0000 (15:24 +0000)]
Rahmem für die CC-Analyse

5 years agoMore complete trivial Arity Analysis
Joachim Breitner [Wed, 22 Oct 2014 11:36:21 +0000 (11:36 +0000)]
More complete trivial Arity Analysis

5 years agoMore general ArityAnalysisPreImpl
Joachim Breitner [Fri, 17 Oct 2014 14:54:58 +0000 (14:54 +0000)]
More general ArityAnalysisPreImpl

5 years agoTowards a CoCall Analysis
Joachim Breitner [Fri, 17 Oct 2014 14:14:06 +0000 (14:14 +0000)]
Towards a CoCall Analysis

5 years agoMore Arity Analysis refactoring
Joachim Breitner [Fri, 17 Oct 2014 14:14:00 +0000 (14:14 +0000)]
More Arity Analysis refactoring

5 years agoMove subst_transform to AbstractTransform
Joachim Breitner [Thu, 16 Oct 2014 14:48:03 +0000 (14:48 +0000)]
Move subst_transform to AbstractTransform

5 years agoMore theory shuffling around
Joachim Breitner [Thu, 16 Oct 2014 11:20:34 +0000 (11:20 +0000)]
More theory shuffling around

5 years agoAttempt at AbstractCorrectness (doomed, due to indeterminism)
Joachim Breitner [Thu, 16 Oct 2014 10:58:21 +0000 (10:58 +0000)]
Attempt at AbstractCorrectness (doomed, due to indeterminism)

5 years agoMerge ArityEtaExpandInst into ArityEtaExpand
Joachim Breitner [Thu, 16 Oct 2014 09:57:40 +0000 (09:57 +0000)]
Merge ArityEtaExpandInst into ArityEtaExpand

5 years agoMove Sestoft-Related eta-expansion away
Joachim Breitner [Thu, 16 Oct 2014 09:52:51 +0000 (09:52 +0000)]
Move Sestoft-Related eta-expansion away

5 years agoSome CoCallGraph stuff
Joachim Breitner [Thu, 16 Oct 2014 09:33:19 +0000 (09:33 +0000)]
Some CoCallGraph stuff

5 years agocont_pt is enough
Joachim Breitner [Thu, 16 Oct 2014 09:32:44 +0000 (09:32 +0000)]
cont_pt is enough

5 years agoAEstack not needed
Joachim Breitner [Thu, 16 Oct 2014 09:32:24 +0000 (09:32 +0000)]
AEstack not needed

5 years agoFix some imports
Joachim Breitner [Thu, 16 Oct 2014 09:31:55 +0000 (09:31 +0000)]
Fix some imports

5 years agoLate saving
Joachim Breitner [Tue, 14 Oct 2014 15:09:44 +0000 (15:09 +0000)]
Late saving

5 years agoMinor cleanup
Joachim Breitner [Tue, 14 Oct 2014 14:16:32 +0000 (14:16 +0000)]
Minor cleanup

5 years agoRe-implement arity-based eta-expansion using AbstractTransform
Joachim Breitner [Tue, 14 Oct 2014 13:58:10 +0000 (13:58 +0000)]
Re-implement arity-based eta-expansion using AbstractTransform

5 years agoTowards more abstract transformation code
Joachim Breitner [Wed, 8 Oct 2014 12:46:35 +0000 (12:46 +0000)]
Towards more abstract transformation code

5 years agoABinds also not required
Joachim Breitner [Mon, 6 Oct 2014 14:33:31 +0000 (14:33 +0000)]
ABinds also not required

5 years agoMove Afix definition out of the way
Joachim Breitner [Mon, 6 Oct 2014 14:29:44 +0000 (14:29 +0000)]
Move Afix definition out of the way

5 years agoSestoftNU
Joachim Breitner [Mon, 6 Oct 2014 13:31:27 +0000 (13:31 +0000)]
SestoftNU

6 years agoAdd a flag to the Var constructor
Joachim Breitner [Tue, 30 Sep 2014 13:25:13 +0000 (13:25 +0000)]
Add a flag to the Var constructor

6 years agoAvoid list_all
Joachim Breitner [Tue, 30 Sep 2014 12:13:00 +0000 (12:13 +0000)]
Avoid list_all

6 years agoSeparate CorrectArityAnalysisLet
Joachim Breitner [Tue, 30 Sep 2014 11:06:32 +0000 (11:06 +0000)]
Separate CorrectArityAnalysisLet

6 years agoMinor wiggling of ArityEtaExpand
Joachim Breitner [Tue, 30 Sep 2014 10:15:22 +0000 (10:15 +0000)]
Minor wiggling of ArityEtaExpand

6 years agoIntroduce step_induction, to avoid the unpleasent intermediate step with variables
Joachim Breitner [Wed, 24 Sep 2014 14:22:30 +0000 (14:22 +0000)]
Introduce step_induction, to avoid the unpleasent intermediate step with variables

6 years agoBack to two variable rules in the Launchbury semantics
Joachim Breitner [Wed, 24 Sep 2014 11:15:58 +0000 (11:15 +0000)]
Back to two variable rules in the Launchbury semantics

6 years agoAdd later_uniqueI
Joachim Breitner [Wed, 24 Sep 2014 11:15:30 +0000 (11:15 +0000)]
Add later_uniqueI

6 years agoRemove constant parameter from eventually
Joachim Breitner [Wed, 24 Sep 2014 08:02:00 +0000 (08:02 +0000)]
Remove constant parameter from eventually

6 years agoAn idea for a look-ahead-simulation-proof
Joachim Breitner [Tue, 23 Sep 2014 13:20:22 +0000 (13:20 +0000)]
An idea for a look-ahead-simulation-proof

6 years agoDeadCodeRemoval2CorrectSestoft is broken
Joachim Breitner [Tue, 23 Sep 2014 11:09:19 +0000 (11:09 +0000)]
DeadCodeRemoval2CorrectSestoft is broken

6 years agoAvoid useless quotation marks
Joachim Breitner [Tue, 23 Sep 2014 09:12:51 +0000 (09:12 +0000)]
Avoid useless quotation marks

6 years agoCreate a ROOT entry for Arity stuff
Joachim Breitner [Tue, 23 Sep 2014 08:58:37 +0000 (08:58 +0000)]
Create a ROOT entry for Arity stuff

6 years ago(simple) Arity analysis correct!
Joachim Breitner [Thu, 7 Aug 2014 14:39:28 +0000 (14:39 +0000)]
(simple) Arity analysis correct!

6 years agoArityEtaExpansion: Es fehlen noch Lemmas zu subst bzw. Aexp und Aheap
Joachim Breitner [Thu, 7 Aug 2014 11:52:07 +0000 (11:52 +0000)]
ArityEtaExpansion: Es fehlen noch Lemmas zu subst bzw. Aexp und Aheap

6 years agoRefactor: map_transform
Joachim Breitner [Wed, 6 Aug 2014 14:45:09 +0000 (14:45 +0000)]
Refactor: map_transform

6 years agoMake Arity Analysis thunk-aware
Joachim Breitner [Wed, 6 Aug 2014 12:52:14 +0000 (12:52 +0000)]
Make Arity Analysis thunk-aware

6 years agoisLam_Aeta_expand_transform
Joachim Breitner [Wed, 6 Aug 2014 09:28:42 +0000 (09:28 +0000)]
isLam_Aeta_expand_transform

6 years agoArity-based eta-expansion proof done (assuming a suitable Aeta_expand_transform)
Joachim Breitner [Wed, 6 Aug 2014 09:19:45 +0000 (09:19 +0000)]
Arity-based eta-expansion proof done (assuming a suitable Aeta_expand_transform)

6 years agoAnother shot at an arity expansion proof
Joachim Breitner [Tue, 5 Aug 2014 15:21:08 +0000 (15:21 +0000)]
Another shot at an arity expansion proof

6 years agoRemoving some comments
Joachim Breitner [Mon, 4 Aug 2014 11:17:53 +0000 (11:17 +0000)]
Removing some comments

6 years agoAll sorries in ArityCorrectSestoft gone
Joachim Breitner [Fri, 1 Aug 2014 13:00:00 +0000 (13:00 +0000)]
All sorries in ArityCorrectSestoft gone

6 years agoHopefully sufficient conditions? (ArityCorrect2 locale)
Joachim Breitner [Fri, 1 Aug 2014 12:38:57 +0000 (12:38 +0000)]
Hopefully sufficient conditions? (ArityCorrect2 locale)

6 years agoA more sensible way to prove correctness of the Arity Analysis
Joachim Breitner [Thu, 31 Jul 2014 14:26:11 +0000 (14:26 +0000)]
A more sensible way to prove correctness of the Arity Analysis