darcs-mirror-isa-launchbury.git
4 years agoAdd a drop rule to SestoftGC master
Joachim Breitner [Tue, 3 Feb 2015 12:56:38 +0000 (12:56 +0000)]
Add a drop rule to SestoftGC

4 years agoFix end-to-end proof to finally obtain the unmodified semantics
Joachim Breitner [Wed, 28 Jan 2015 13:02:12 +0000 (13:02 +0000)]
Fix end-to-end proof to finally obtain the unmodified semantics

4 years agoRemove some dead code
Joachim Breitner [Tue, 27 Jan 2015 09:56:50 +0000 (09:56 +0000)]
Remove some dead code

4 years agoCorrectness via card, ugly proof from GCstep to step (up to renaming)
Joachim Breitner [Mon, 26 Jan 2015 09:39:21 +0000 (09:39 +0000)]
Correctness via card, ugly proof from GCstep to step (up to renaming)

4 years agoNo need for heap_upds_ok in EtaExpandCorrect
Joachim Breitner [Tue, 20 Jan 2015 14:36:02 +0000 (14:36 +0000)]
No need for heap_upds_ok in EtaExpandCorrect

4 years agoSeparate Arity consistency from Cardinality consistency
Joachim Breitner [Tue, 20 Jan 2015 14:32:01 +0000 (14:32 +0000)]
Separate Arity consistency from Cardinality consistency

4 years agoFinish CardinalityetaExpandCorrect with IfThenElse
Joachim Breitner [Fri, 16 Jan 2015 15:50:26 +0000 (15:50 +0000)]
Finish CardinalityetaExpandCorrect with IfThenElse

4 years agoSwitch to Bool b; prepare CardinalityetaExpandCorrect with the new cases
Joachim Breitner [Fri, 16 Jan 2015 11:59:08 +0000 (11:59 +0000)]
Switch to Bool b; prepare CardinalityetaExpandCorrect with the new cases

4 years agoPrepare CardinalityEtaExpand for a stack with expressions
Joachim Breitner [Fri, 16 Jan 2015 10:29:31 +0000 (10:29 +0000)]
Prepare CardinalityEtaExpand for a stack with expressions

4 years agoUse isVal everywhere
Joachim Breitner [Thu, 15 Jan 2015 15:10:17 +0000 (15:10 +0000)]
Use isVal everywhere

4 years agoAdd Null and (e ? e : e)
Joachim Breitner [Thu, 15 Jan 2015 13:25:49 +0000 (13:25 +0000)]
Add Null and (e ? e : e)

4 years agoGet rid of GVar detour
Joachim Breitner [Thu, 15 Jan 2015 12:37:50 +0000 (12:37 +0000)]
Get rid of GVar detour

4 years agoForgotten theory before-adding-ifthenelse
Joachim Breitner [Thu, 15 Jan 2015 12:10:46 +0000 (12:10 +0000)]
Forgotten theory

4 years agoAdd forgotten ArityEtaExpand
Joachim Breitner [Thu, 15 Jan 2015 12:02:46 +0000 (12:02 +0000)]
Add forgotten ArityEtaExpand

4 years agoMore module splitting
Joachim Breitner [Thu, 15 Jan 2015 11:30:24 +0000 (11:30 +0000)]
More module splitting

4 years agoAvoid theory-level interpretation
Joachim Breitner [Wed, 14 Jan 2015 18:14:49 +0000 (18:14 +0000)]
Avoid theory-level interpretation

4 years agoSplit CoCallCardinality into CoCall* modules
Joachim Breitner [Wed, 14 Jan 2015 16:19:03 +0000 (16:19 +0000)]
Split CoCallCardinality into CoCall* modules

4 years agoModules FTreeAnalysisSig, FTreeAnalysisSpec
Joachim Breitner [Wed, 14 Jan 2015 16:00:10 +0000 (16:00 +0000)]
Modules FTreeAnalysisSig, FTreeAnalysisSpec

4 years agoUnused import
Joachim Breitner [Wed, 14 Jan 2015 15:50:54 +0000 (15:50 +0000)]
Unused import

4 years agoModule name: CoCallAnalysisSig
Joachim Breitner [Wed, 14 Jan 2015 15:50:09 +0000 (15:50 +0000)]
Module name: CoCallAnalysisSig

4 years agoGet rid of ccExp'
Joachim Breitner [Wed, 14 Jan 2015 15:46:08 +0000 (15:46 +0000)]
Get rid of ccExp'

4 years agoGet rid of Aexp'
Joachim Breitner [Wed, 14 Jan 2015 15:30:15 +0000 (15:30 +0000)]
Get rid of Aexp'

4 years agoSome module reorganization
Joachim Breitner [Wed, 14 Jan 2015 15:05:13 +0000 (15:05 +0000)]
Some module reorganization

4 years agoUnused locale
Joachim Breitner [Tue, 13 Jan 2015 10:34:08 +0000 (10:34 +0000)]
Unused locale

4 years agoRemove more commented code
Joachim Breitner [Tue, 13 Jan 2015 10:32:45 +0000 (10:32 +0000)]
Remove more commented code

4 years agoRemove some commented code
Joachim Breitner [Tue, 13 Jan 2015 10:27:31 +0000 (10:27 +0000)]
Remove some commented code

4 years agoExample end-to-end transformation
Joachim Breitner [Mon, 12 Jan 2015 10:31:59 +0000 (10:31 +0000)]
Example end-to-end transformation

4 years agoChange parameter of ccNeighbors to a variable
Joachim Breitner [Mon, 12 Jan 2015 10:31:40 +0000 (10:31 +0000)]
Change parameter of ccNeighbors to a variable

4 years agoAexp_restr_subst and CCexp_subst mutual recursive. No sorries! Perfect for friday...
Joachim Breitner [Fri, 9 Jan 2015 16:16:01 +0000 (16:16 +0000)]
Aexp_restr_subst and CCexp_subst mutual recursive. No sorries! Perfect for friday evening.

4 years agoAexp_subst_upd can be derived from Aexp_subst, move to locale
Joachim Breitner [Fri, 9 Jan 2015 13:37:42 +0000 (13:37 +0000)]
Aexp_subst_upd can be derived from Aexp_subst, move to locale

4 years agoLess aggressive ccBindsExtra
Joachim Breitner [Fri, 9 Jan 2015 09:47:04 +0000 (09:47 +0000)]
Less aggressive ccBindsExtra

4 years agoMake use of wild_recursion_thunked
Joachim Breitner [Fri, 9 Jan 2015 09:36:30 +0000 (09:36 +0000)]
Make use of wild_recursion_thunked

4 years agoPartial work adding nonrecursive bindings as well; very ugly so far.
Joachim Breitner [Thu, 8 Jan 2015 17:00:16 +0000 (17:00 +0000)]
Partial work adding nonrecursive bindings as well; very ugly so far.

4 years agoAdd a wild_recursion variant that caters for thunks
Joachim Breitner [Thu, 8 Jan 2015 17:00:03 +0000 (17:00 +0000)]
Add a wild_recursion variant that caters for thunks

4 years agoMake wild_recursion weaker
Joachim Breitner [Thu, 8 Jan 2015 16:59:40 +0000 (16:59 +0000)]
Make wild_recursion weaker

4 years agoAdd non-rec case to the implementation
Joachim Breitner [Wed, 7 Jan 2015 14:15:13 +0000 (14:15 +0000)]
Add non-rec case to the implementation

4 years agoBack to edom ae = edom ce
Joachim Breitner [Wed, 7 Jan 2015 12:22:06 +0000 (12:22 +0000)]
Back to edom ae = edom ce

4 years agoFix NoCardinalityAnalysis.thy a bit, but still broken
Joachim Breitner [Wed, 7 Jan 2015 09:54:23 +0000 (09:54 +0000)]
Fix NoCardinalityAnalysis.thy a bit, but still broken

4 years agoEnd-to-end theory for sanity checking
Joachim Breitner [Wed, 7 Jan 2015 09:43:05 +0000 (09:43 +0000)]
End-to-end theory for sanity checking

4 years agoDefine non-recursive bindings
Joachim Breitner [Wed, 7 Jan 2015 09:42:47 +0000 (09:42 +0000)]
Define non-recursive bindings

4 years agoAllow ae and ce to differ in their domain. Ugly, but works.
Joachim Breitner [Mon, 5 Jan 2015 14:54:26 +0000 (14:54 +0000)]
Allow ae and ce to differ in their domain. Ugly, but works.

4 years agoExtract FTreeAnalysis
Joachim Breitner [Mon, 5 Jan 2015 11:27:40 +0000 (11:27 +0000)]
Extract FTreeAnalysis

4 years agoDemand more in FutureAnalysisCarrier
Joachim Breitner [Fri, 19 Dec 2014 15:29:47 +0000 (15:29 +0000)]
Demand more in FutureAnalysisCarrier

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

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

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

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

4 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 _?_:_)

4 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

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

4 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

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

4 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

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

4 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.

4 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

4 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

4 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

4 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!

4 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

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

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

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

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

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

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

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

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

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

4 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

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

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

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

4 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

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

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

4 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

4 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

4 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

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

4 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

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

4 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

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

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

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

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

4 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

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

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

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

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

4 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

4 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...

4 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

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

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

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

4 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

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