Commit Graph

214 Commits

Author SHA1 Message Date
Andreas Stadelmeier
a0d98b9403 Make match rule remember constraint type 2024-02-13 18:40:39 +01:00
Andreas Stadelmeier
fca93d7ec6 Introduce normal type placeholders \ntv 2024-02-12 15:28:44 +01:00
Andreas Stadelmeier
5074c21943 Cleanup 2024-02-11 23:30:09 +01:00
Andreas Stadelmeier
cbd0a48ca6 Add T-Call rule without receiver 2024-02-11 23:29:34 +01:00
Andreas Stadelmeier
3017cfc796 Introduction Wildcards 2024-02-11 21:59:57 +01:00
Andreas Stadelmeier
813b256e4d Intro to type rules 2024-02-10 08:19:24 +01:00
Andreas Stadelmeier
7ed1529710 Include Adopt, Settle and Raise again 2024-02-10 08:18:58 +01:00
JanUlrich
669837d6ac Remove unnecessary fv premisses 2024-02-09 21:49:41 +01:00
JanUlrich
3f92215914 Intro to Type Rules 2024-02-09 21:49:12 +01:00
Andreas Stadelmeier
1a3cf1c78e Change equals 2024-02-08 14:53:40 +01:00
Andreas Stadelmeier
7bf8a3a2da Add Trim method 2024-02-08 10:49:03 +01:00
Andreas Stadelmeier
10fcfcfea0 Cleanup Introduction. Fix method environment in Type Rules 2024-02-07 18:26:41 +01:00
Andreas Stadelmeier
26678767c2 Cleanup, rephrase introduction. Fix and Cleanup type rules. Remove override 2024-02-07 17:29:41 +01:00
JanUlrich
6c716c5138 Add to introduction 2024-02-07 10:28:28 +01:00
Andreas Stadelmeier
f40299a36c hange Equals rule. Add explanations 2024-02-06 18:05:05 +01:00
JanUlrich
98a66bbced Add Wildcard introduction 2024-02-06 09:45:53 +01:00
Andreas Stadelmeier
5433e94aab Fixes 2024-02-06 00:44:48 +01:00
JanUlrich
faf7df709a Remove circle. Change input requirements 2024-02-05 19:18:16 +01:00
JanUlrich
f54f4b449d Cleanup and fixes 2024-02-05 17:15:34 +01:00
Andreas Stadelmeier
df119b1995 Merge branch 'master' of ssh://gitea.hb.dhbw-stuttgart.de:2222/stan/Ecoop2024_TIforWildFJ 2024-02-05 14:54:46 +01:00
Andreas Stadelmeier
43e75127b3 Nearly finish soundness for TYPE 2024-02-05 14:54:42 +01:00
JanUlrich
5c73e0b0f8 Remove Settle and Raise rules 2024-02-05 01:33:39 +01:00
Andreas Stadelmeier
3d10421439 Remove adopt. Add Gen-X to Unify 2024-02-02 19:23:00 +01:00
Andreas Stadelmeier
c53f1b59af Merge branch 'master' of ssh://gitea.hb.dhbw-stuttgart.de:2222/stan/Ecoop2024_TIforWildFJ 2024-02-02 13:23:02 +01:00
Andreas Stadelmeier
67ce9e42a2 Fixes 2024-02-02 13:22:55 +01:00
JanUlrich
743e32daa9 Use Unify recursive in method call soundness proof 2024-02-01 18:17:46 +01:00
Andreas Stadelmeier
edc7f87108 Type Soundness 2024-02-01 14:54:44 +01:00
Andreas Stadelmeier
3716fcdfd1 Type soundness 2024-01-31 18:06:04 +01:00
Andreas Stadelmeier
4725943448 Change = \emptyset to \subseteq Delta 2024-01-31 18:05:42 +01:00
Andreas Stadelmeier
921adc85b1 Start let insert example 2024-01-31 18:05:22 +01:00
Andreas Stadelmeier
8e3707b9a6 WF lemma 2024-01-31 07:51:17 +01:00
Andreas Stadelmeier
54fb6f9f0f Fix Unify WF lemma 2024-01-30 23:03:34 +01:00
Andreas Stadelmeier
319f080a8d Add LessdotCC REmove to unify. Fix Soundness lemma 2024-01-30 16:19:01 +01:00
JanUlrich
9aa89933ce Add WF type environment lemma (work in progress) 2024-01-29 18:44:21 +01:00
JanUlrich
95d0d00339 Fix WF-Class, WF-Var and Type for method call 2024-01-29 18:39:18 +01:00
Andreas Stadelmeier
6494394db6 Comments on Well-Formedness proof 2024-01-29 13:41:12 +01:00
Andreas Stadelmeier
0101341841 Fix and comment 2024-01-26 16:50:56 +01:00
JanUlrich
ba4b78b57b Soundness method call 2024-01-24 13:18:48 +01:00
Andreas Stadelmeier
05b6b84e1e Cleanup soundness. Add Delta environment to Unify input 2024-01-23 16:30:24 +01:00
Andreas Stadelmeier
881eecef8a Add <._c constraint to Type for field and alter soundness proof 2024-01-23 00:34:48 +01:00
Andreas Stadelmeier
b775045d17 Soundness for Prepare and Capture 2024-01-22 15:34:33 +01:00
Andreas Stadelmeier
e3a393520d fix capture soundness proof 2024-01-22 01:03:58 +01:00
Andreas Stadelmeier
ba8e2fadbb Add Capture Conversion during unification chapter 2024-01-21 14:31:48 +01:00
Andreas Stadelmeier
5578415ed3 Fix Capture Soundness 2024-01-17 12:53:36 +01:00
Andreas Stadelmeier
8907cac94a Prepare Soundness 2024-01-17 10:58:16 +01:00
JanUlrich
56f9d35615 Change prepare rule to require same type on both sides 2024-01-17 05:52:01 +01:00
Andreas Stadelmeier
bc4fcaf43c Change Prepare rule to simpler version 2024-01-16 18:03:54 +01:00
JanUlrich
521dee7fa2 Soundness Prepare 2024-01-16 10:00:47 +01:00
Andreas Stadelmeier
b546da831d Start soundness for prepare rule 2024-01-15 20:43:19 +01:00
Andreas Stadelmeier
b9e0b1fa6d Fix error in Prepare rule 2024-01-15 20:43:06 +01:00