darcs-mirror-isa-launchbury.git
5 years agoRemove some dead code
Joachim Breitner [Tue, 27 Jan 2015 09:56:50 +0000 (09:56 +0000)]
Remove some dead code

5 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)

5 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

5 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

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

5 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

5 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

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

5 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)

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

5 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

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

5 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

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

5 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

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

5 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

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

5 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

5 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

5 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

5 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

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

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

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

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