@@ -358,112 +387,46 @@
| component |
plane |
files |
-
-
- |
-
-
- |
|
- | rt-transition |
- t-bound context-sensitive rt-transition |
- lfpr ( â¦?,?⦠⢠â¡[?,?] ? ) |
- lfpr_length lfpr_drops lfpr_fqup lfpr_lfpx lfpr_lfpr |
-
-
- |
-
-
- |
+ rt-transition |
+ counted context-sensitive rt-transition |
+ cpg ( â¦?,?⦠⢠? â¬[?,?] ? ) |
+ cpg_simple cpg_drops cpg_lsubr |
-
-
- |
-
-
- |
- cpr ( â¦?,?⦠⢠? â¡[?] ? ) |
- cpr_drops |
-
-
- |
-
-
- |
+ iterated static typing |
+ iterated extension on referred entries |
+ tc_lfxs ( ? ⦻**[?,?] ? ) |
+ tc_lfxs_length tc_lfxs_drops tc_lfxs_fqup tc_lfxs_tc_lfxs |
-
-
- |
-
-
- |
- cpm ( â¦?,?⦠⢠? â¡[?,?] ? ) |
- cpm_simple cpm_drops cpm_lsubr cpm_cpx |
-
-
- |
-
-
- |
-
-
-
-
- |
- uncounted context-sensitive rt-transition |
- lfpx ( â¦?,?⦠⢠â¬[?,?] ? ) |
- lfpx_length lfpx_drops lfpx_fqup lfpx_frees |
-
-
- |
-
-
- |
+ static typing |
+ generic reducibility |
+ lsubc ( ? ⢠? â«[?] ? ) |
+ lsubc_drops lsubc_lsubr lsubc_lsuba |
-
-
- |
-
-
- |
- cpx ( â¦?,?⦠⢠? â¬[?] ? ) |
- cpx_simple cpx_drops cpx_lsubr |
-
+ |
|
-
+ |
|
+ gcp_cr ( â¦?,?,?⦠ϵ[?] ã?ã ) |
+ gcp_aaa |
-
-
- |
- counted context-sensitive rt-transition |
- cpg ( â¦?,?⦠⢠? â¬[?,?] ? ) |
- cpg_simple cpg_drops cpg_lsubr |
-
-
- |
-
+ |
|
-
-
- | static typing |
- parameters |
- sh |
- sd |
-
+ |
|
+ gcp |
|
@@ -472,57 +435,37 @@
|
- restricted ref. for atomic arity assignment |
+ atomic arity assignment |
lsuba ( ? ⢠? â«â ? ) |
- lsuba_drops lsuba_lsubr lsuba_aaa lsuba_lsuba |
-
-
- |
-
-
- |
+ lsuba_drops lsuba_lsubr lsuba_aaa lsuba_lsuba |
|
- atomic arity assignment |
- aaa ( â¦?,?⦠⢠? â ? ) |
- aaa_drops aaa_fqus aaa_lfeq aaa_aaa |
-
-
- |
-
+ |
|
+ aaa ( â¦?,?⦠⢠? â ? ) |
+ aaa_drops aaa_fqus aaa_lfdeq aaa_aaa |
|
- equivalence for closures on referred entries |
- ffeq ( �,?,?⦠⡠�,?,?⦠) |
- ffeq_freq |
-
-
- |
-
-
- |
+ degree-based equivalence on referred entries |
+ ffdeq ( â¦?,?,?⦠â¡[?,?] â¦?,?,?⦠) |
+ ffdeq_fqup ffdeq_ffdeq |
|
- equivalence for local environments on referred entries |
- lfeq ( ? â¡[?] ? ) |
- lfeq_length lfeq_lreq lfeq_fqup lfeq_lfeq |
-
-
- |
-
+ |
|
+ lfdeq ( ? â¡[?,?,?] ? ) |
+ lfdeq_length lfdeq_drops lfdeq_fqup lfdeq_fqus lfdeq_lfdeq |
|
@@ -530,41 +473,25 @@
|
generic extension on referred entries |
lfxs ( ? ⦻*[?,?] ? ) |
- lfxs_length lfxs_drops lfxs_fqup lfxs_lfxs |
-
-
- |
-
-
- |
+ lfxs_length lfxs_drops lfxs_fqup lfxs_lfxs |
|
- restricted ref. for context-sensitive free variables |
+ context-sensitive free variables |
lsubf ( â¦?,?⦠â«ð
* �,?⦠) |
- lsubf_frees |
-
-
- |
-
-
- |
+ lsubf_lsubr lsubf_frees lsubf_lsubf |
|
- context-sensitive free variables |
- frees ( ? ⢠ð
*�⦠⡠? ) |
- frees_weight frees_lreq frees_drops frees_fqup frees_fqus frees_frees |
-
-
- |
-
+ |
|
+ frees ( ? ⢠ð
*�⦠⡠? ) |
+ frees_drops frees_fqup frees_frees |
|
@@ -572,25 +499,13 @@
|
restricted ref. for local env. |
lsubr ( ? â« ? ) |
- lsubr_length lsubr_drops lsubr_lsubr |
-
-
- |
-
-
- |
+ lsubr_length lsubr_drops lsubr_lsubr |
| s-computation |
iterated structural successor for closures |
- fqus ( â¦?,?,?⦠â* â¦?,?,?⦠) |
- fqus_weight fqus_drops fqus_fqup fqus_fqus |
-
-
- |
-
-
- |
+ fqus ( â¦?,?,?⦠â*[?] â¦?,?,?⦠) ( â¦?,?,?⦠â* â¦?,?,?⦠) |
+ fqus_weight fqus_drops fqus_fqup fqus_fqus |
|
@@ -599,26 +514,14 @@
|
|
- fqup ( â¦?,?,?⦠â+ â¦?,?,?⦠) |
- fqup_weight fqup_drops fqup_fqup |
-
-
- |
-
-
- |
+ fqup ( â¦?,?,?⦠â+[?] â¦?,?,?⦠) ( â¦?,?,?⦠â+ â¦?,?,?⦠) |
+ fqup_weight fqup_drops fqup_fqup |
| s-transition |
structural successor for closures |
- fquq ( â¦?,?,?⦠â⸮ â¦?,?,?⦠) |
- fquq_length fquq_weight |
-
-
- |
-
-
- |
+ fquq ( â¦?,?,?⦠â⸮[?] â¦?,?,?⦠) ( â¦?,?,?⦠â⸮ â¦?,?,?⦠) |
+ fquq_length fquq_weight |
|
@@ -627,25 +530,13 @@
|
|
- fqu ( â¦?,?,?⦠â â¦?,?,?⦠) |
- fqu_length fqu_weight |
-
-
- |
-
-
- |
+ fqu ( â¦?,?,?⦠â[?] â¦?,?,?⦠) ( â¦?,?,?⦠â â¦?,?,?⦠) |
+ fqu_length fqu_weight |
| relocation |
generic slicing for local environments |
drops_vector ( â¬*[?,?] ? â¡ ? ) ( â¬*[?] ? â¡ ? ) |
-
-
- |
-
-
- |
|
@@ -658,80 +549,124 @@
drops ( â¬*[?,?] ? â¡ ? ) ( â¬*[?] ? â¡ ? ) |
- drops_lstar drops_weight drops_length drops_ceq drops_lexs drops_lreq drops_drops |
-
+ | drops_lstar drops_weight drops_length drops_ext2 drops_lexs drops_lreq drops_drops |
+
+
+
|
-
+ | generic relocation |
+ lifts_bind ( â¬*[?] ? â¡ ? ) |
+ lifts_weight_bind lifts_lifts_bind |
+
+
+
+
+ |
+
|
+ lifts_vector ( â¬*[?] ? â¡ ? ) |
+ lifts_lifts_vector |
|
- generic relocation for terms |
- lifts_vector ( â¬*[?] ? â¡ ? ) |
- lifts_lifts_vector |
-
+ |
|
-
+ | lifts ( â¬*[?] ? â¡ ? ) |
+ lifts_simple lifts_weight lifts_tdeq lifts_lifts |
+
+
+
|
+ ranged equivalence for local environments |
+ lreq ( ? â¡[?] ? ) |
+ lreq_length lreq_lreq |
|
-
+ | generic entrywise extension |
+ lexs ( ? ⦻*[?,?,?] ? ) |
+ lexs_length lexs_lexs |
+
+
+ | syntax |
+ append for local environments |
+ append ( ? @@ ? ) |
+ append_length |
+
+
+
|
- lifts ( â¬*[?] ? â¡ ? ) |
- lifts_simple lifts_weight lifts_lifts |
-
+ | head equivalence for terms |
+ theq ( ? ⩳[?,?] ? ) |
+ theq_simple theq_tdeq theq_theq theq_simple_vector |
+
+
+
|
-
+ | degree-based equivalence |
+ tdeq_ext ( ? â¡[?,?] ? ) |
+
|
- |
+ |
|
- ranged equivalence for local environments |
- lreq ( ? â¡[?] ? ) |
- lreq_length lreq_lreq |
-
+ |
|
-
+ | tdeq ( ? â¡[?,?] ? ) |
+ tdeq_tdeq |
+
+
+
+
+ |
+ closures |
+ cl_weight ( â¯{?,?,?} ) |
+
|
- |
+ |
|
- generic entrywise extension |
- lexs ( ? ⦻*[?,?,?] ? ) |
- lexs_length lexs_lexs |
-
+ |
|
-
+ | cl_restricted_weight ( â¯{?,?} ) |
+
|
- | grammar |
- append for local environments |
- append ( ? @@ ? ) |
- append_length |
-
+ |
+
+ |
+ global environments |
+ genv |
+
+
+ |
+
+
+
|
+ local environments |
+ lenv_ext2 |
|
@@ -740,12 +675,10 @@
|
- context-sensitive equivalences for terms |
- ceq |
- ceq_ceq |
-
+ |
|
+ lenv_length ( |?| ) |
|
@@ -754,12 +687,10 @@
|
- same top term structure |
- tsts ( ? â ? ) |
- tsts_tsts tsts_vector |
-
+ |
|
+ lenv_weight ( â¯{?} ) |
|
@@ -768,12 +699,10 @@
|
- closures |
- cl_weight ( â¯{?,?,?} ) |
- cl_restricted_weight ( â¯{?,?} ) |
-
+ |
|
+ lenv |
|
@@ -782,14 +711,26 @@
|
- internal syntax |
- genv |
-
+ | binders for local environments |
+ ext2 |
+ ext2_ext2 |
+
+
+
|
-
+ |
|
+ bind |
+ bind_weight |
+
+
+
+
+ |
+ terms |
+ term_vector ( �.? ) |
|
@@ -801,9 +742,7 @@
|
- lenv |
- lenv_weight ( â¯{?} ) |
- lenv_length ( |?| ) |
+ term_simple ( ðâ¦?⦠) |
|
@@ -815,10 +754,10 @@
|
- term |
- term_weight ( â¯{?} ) |
- term_simple ( ðâ¦?⦠) |
- term_vector ( �.? ) |
+ term_weight ( â¯{?} ) |
+
+
+ |
|
@@ -827,29 +766,51 @@
|
|
- item |
-
+ | term |
+
|
-
+ |
+
+
|
+ items |
+ item_sd |
|
- |
+ |
|
- external syntax |
- aarity |
-
+ |
+
+ |
+ item_sh |
+
+
+ |
+
+
+
|
-
+ |
|
+ item |
+
+
+ |
+
+
+
+
+ |
+ atomic arities |
+ aarity |
|
@@ -883,6 +844,6 @@
- Last update: Tue, 17 Jan 2017 21:42:42 +0100
+ Last update: Tue, 17 Oct 2017 20:34:24 +0200