Commit a64c9a94 authored by André Pacak's avatar André Pacak

generalization: eliminate infinite non-userinput instead of hard-coded context

parent 49db7751
......@@ -259,7 +259,7 @@
<node concept="1puMqW" id="4RJJaubPgua" role="1puA0r">
<ref role="1puQsG" node="7DdCaEODx6h" resolve="eliminateContextByProjection" />
</node>
<node concept="1puMqW" id="6XUlM2pBoFi" role="1puA0r">
<node concept="1puMqW" id="2iwoW_qGyTa" role="1puA0r">
<ref role="1puQsG" node="6XUlM2nKRm7" resolve="mergeContextProjectionLookup" />
</node>
</node>
......@@ -350,11 +350,11 @@
<node concept="3cpWsn" id="7DdCaEOM$5v" role="3cpWs9">
<property role="TrG5h" value="helper" />
<node concept="3uibUv" id="7DdCaEOM$5w" role="1tU5fm">
<ref role="3uigEE" to="5tos:7DdCaEOHNmh" resolve="EliminateTypeArgumentHelper" />
<ref role="3uigEE" to="5tos:7DdCaEOHNmh" resolve="EliminateTypeArgument" />
</node>
<node concept="2ShNRf" id="7DdCaEOMA9n" role="33vP2m">
<node concept="1pGfFk" id="7DdCaEOMA9m" role="2ShVmc">
<ref role="37wK5l" to="5tos:7DdCaEOLG7S" resolve="EliminateTypeArgumentHelper" />
<ref role="37wK5l" to="5tos:7DdCaEOLG7S" resolve="EliminateTypeArgument" />
<node concept="1Q6Npb" id="7DdCaEOMA9Z" role="37wK5m" />
<node concept="1iwH7S" id="7DdCaEOPTYJ" role="37wK5m" />
<node concept="37vLTw" id="7DdCaEOQ2Vw" role="37wK5m">
......@@ -668,7 +668,7 @@
<ref role="3cqZAo" node="7DdCaEOM$5v" resolve="helper" />
</node>
<node concept="liA8E" id="7DdCaEOTnkB" role="2OqNvi">
<ref role="37wK5l" to="5tos:7DdCaEOOhFm" resolve="getIndexOfTypeSort" />
<ref role="37wK5l" to="5tos:7DdCaEOOhFm" resolve="getIndexSortToEliminate" />
</node>
</node>
</node>
......@@ -1178,11 +1178,11 @@
<node concept="3cpWsn" id="32CDcOyFphS" role="3cpWs9">
<property role="TrG5h" value="projectContext" />
<node concept="3uibUv" id="32CDcOyFphP" role="1tU5fm">
<ref role="3uigEE" to="5tos:32CDcOyEa0d" resolve="ProjectContext" />
<ref role="3uigEE" to="5tos:32CDcOyEa0d" resolve="ProjectNonUserInput" />
</node>
<node concept="2ShNRf" id="32CDcOyFphT" role="33vP2m">
<node concept="1pGfFk" id="32CDcOyFphU" role="2ShVmc">
<ref role="37wK5l" to="5tos:32CDcOyElBr" resolve="ProjectContext" />
<ref role="37wK5l" to="5tos:32CDcOyElBr" resolve="ProjectNonUserInput" />
<node concept="37vLTw" id="4RJJaubf2rm" role="37wK5m">
<ref role="3cqZAo" node="4RJJaubeT55" resolve="module" />
</node>
......@@ -1190,10 +1190,19 @@
</node>
</node>
</node>
<node concept="3clFbH" id="6XUlM2o$mAt" role="3cqZAp" />
<node concept="3SKdUt" id="2iwoW_qlXPJ" role="3cqZAp">
<node concept="3SKdUq" id="2iwoW_qlXPL" role="3SKWNk">
<property role="3SKdUp" value="get all decls with at least two inputs one user and infinite" />
</node>
</node>
<node concept="3SKdUt" id="2iwoW_qoyf8" role="3cqZAp">
<node concept="3SKdUq" id="2iwoW_qoyfa" role="3SKWNk">
<property role="3SKdUp" value="assume only judgments without type input are available" />
</node>
</node>
<node concept="3cpWs8" id="32CDcOyFp__" role="3cqZAp">
<node concept="3cpWsn" id="32CDcOyFp_A" role="3cpWs9">
<property role="TrG5h" value="declsWithContextAndTerm" />
<property role="TrG5h" value="declsWithUserAndNonUserInput" />
<node concept="2I9FWS" id="32CDcOyFp_x" role="1tU5fm">
<ref role="2I9WkF" to="b83y:2_58u12eLDI" resolve="JudgmentDeclaration" />
</node>
......@@ -1201,8 +1210,8 @@
<node concept="37vLTw" id="6XUlM2o$E10" role="2Oq$k0">
<ref role="3cqZAo" node="4RJJaubf6Wq" resolve="querier" />
</node>
<node concept="liA8E" id="4RJJauciBAn" role="2OqNvi">
<ref role="37wK5l" to="5tos:4RJJauchPfF" resolve="getDeclarationsWithTermAndContext" />
<node concept="liA8E" id="2iwoW_qnZcR" role="2OqNvi">
<ref role="37wK5l" to="5tos:2iwoW_qmyLT" resolve="getDeclarationsWithUserAndNonUserInput" />
</node>
</node>
</node>
......@@ -1215,13 +1224,13 @@
</node>
<node concept="3cpWs8" id="32CDcOyY7qv" role="3cqZAp">
<node concept="3cpWsn" id="32CDcOyY7qw" role="3cpWs9">
<property role="TrG5h" value="declarationWithTermAndContext" />
<property role="TrG5h" value="declarationWithUserAndNonUserInput" />
<node concept="3Tqbb2" id="32CDcOyY7qt" role="1tU5fm">
<ref role="ehGHo" to="b83y:2_58u12eLDI" resolve="JudgmentDeclaration" />
</node>
<node concept="2OqwBi" id="4RJJauciILb" role="33vP2m">
<node concept="37vLTw" id="4RJJauciFKk" role="2Oq$k0">
<ref role="3cqZAo" node="32CDcOyFp_A" resolve="declsWithContextAndTerm" />
<ref role="3cqZAo" node="32CDcOyFp_A" resolve="declsWithUserAndNonUserInput" />
</node>
<node concept="1yVyf7" id="4RJJauciP8k" role="2OqNvi" />
</node>
......@@ -1229,7 +1238,7 @@
</node>
<node concept="3cpWs8" id="32CDcOyOAkq" role="3cqZAp">
<node concept="3cpWsn" id="32CDcOyOAkr" role="3cpWs9">
<property role="TrG5h" value="contextProjectionDeclaration" />
<property role="TrG5h" value="nonUserInputProjectionDeclaration" />
<node concept="3Tqbb2" id="32CDcOyOAkd" role="1tU5fm">
<ref role="ehGHo" to="b83y:2_58u12eLDI" resolve="JudgmentDeclaration" />
</node>
......@@ -1238,9 +1247,9 @@
<ref role="3cqZAo" node="32CDcOyFphS" resolve="projectContext" />
</node>
<node concept="liA8E" id="32CDcOyOAku" role="2OqNvi">
<ref role="37wK5l" to="5tos:32CDcOyFaKP" resolve="createContextProjectionDeclaration" />
<ref role="37wK5l" to="5tos:32CDcOyFaKP" resolve="createNonUserInputProjectionDeclaration" />
<node concept="37vLTw" id="32CDcOyY7q$" role="37wK5m">
<ref role="3cqZAo" node="32CDcOyY7qw" resolve="declarationWithTermAndContext" />
<ref role="3cqZAo" node="32CDcOyY7qw" resolve="declarationWithUserAndNonUserInput" />
</node>
</node>
</node>
......@@ -1249,11 +1258,11 @@
<node concept="3clFbF" id="32CDcOyO$IW" role="3cqZAp">
<node concept="2OqwBi" id="32CDcOyOO22" role="3clFbG">
<node concept="37vLTw" id="32CDcOyYana" role="2Oq$k0">
<ref role="3cqZAo" node="32CDcOyY7qw" resolve="declarationWithTermAndContext" />
<ref role="3cqZAo" node="32CDcOyY7qw" resolve="declarationWithUserAndNonUserInput" />
</node>
<node concept="HtI8k" id="32CDcOyOQzp" role="2OqNvi">
<node concept="37vLTw" id="32CDcOyOQ$5" role="HtI8F">
<ref role="3cqZAo" node="32CDcOyOAkr" resolve="contextProjectionDeclaration" />
<ref role="3cqZAo" node="32CDcOyOAkr" resolve="nonUserInputProjectionDeclaration" />
</node>
</node>
</node>
......@@ -1301,6 +1310,11 @@
<property role="3SKdUp" value="only consider instances in premise of rules" />
</node>
</node>
<node concept="3SKdUt" id="2iwoW_q$7Fm" role="3cqZAp">
<node concept="3SKdUq" id="2iwoW_q$7Fo" role="3SKWNk">
<property role="3SKdUp" value="TODO better way than searching for name?" />
</node>
</node>
<node concept="3cpWs8" id="4RJJaucccN1" role="3cqZAp">
<node concept="3cpWsn" id="4RJJaucccN2" role="3cpWs9">
<property role="TrG5h" value="instancesNoRequired" />
......@@ -1423,7 +1437,7 @@
<ref role="3cqZAo" node="32CDcOyFphS" resolve="projectContext" />
</node>
<node concept="liA8E" id="4RJJaubxenX" role="2OqNvi">
<ref role="37wK5l" to="5tos:4RJJaubx95f" resolve="createContextProjectionRule" />
<ref role="37wK5l" to="5tos:4RJJaubx95f" resolve="createNonUserInputProjectionRule" />
<node concept="37vLTw" id="4RJJaubxenY" role="37wK5m">
<ref role="3cqZAo" node="4RJJaubx5V5" resolve="instance" />
</node>
......@@ -1468,67 +1482,28 @@
</node>
</node>
<node concept="37vLTw" id="4RJJaubx4ag" role="1DdaDG">
<ref role="3cqZAo" node="32CDcOyFp_A" resolve="declsWithContextAndTerm" />
<ref role="3cqZAo" node="32CDcOyFp_A" resolve="declsWithUserAndNonUserInput" />
</node>
</node>
<node concept="3clFbH" id="4RJJaucpsk3" role="3cqZAp" />
<node concept="3clFbH" id="4RJJaucpxLG" role="3cqZAp" />
<node concept="3SKdUt" id="4RJJaucl7lB" role="3cqZAp">
<node concept="3SKdUq" id="4RJJaucl7lD" role="3SKWNk">
<property role="3SKdUp" value="replace declarations with context with declarations without (and instances)" />
<property role="3SKdUp" value="replace declarations with nonuserinput with declarations without (and instances)" />
</node>
</node>
<node concept="1DcWWT" id="4RJJauckL4V" role="3cqZAp">
<node concept="3clFbS" id="4RJJauckL4W" role="2LFqv$">
<node concept="3cpWs8" id="4RJJaubT8g8" role="3cqZAp">
<node concept="3cpWsn" id="4RJJaubT8g9" role="3cpWs9">
<property role="TrG5h" value="contextIndex" />
<node concept="10Oyi0" id="4RJJaubT8g6" role="1tU5fm" />
<node concept="2OqwBi" id="4RJJaubT8ga" role="33vP2m">
<node concept="37vLTw" id="4RJJaubT8gb" role="2Oq$k0">
<ref role="3cqZAo" node="4RJJauckL5H" resolve="decl" />
</node>
<node concept="2qgKlT" id="4RJJaubT8gc" role="2OqNvi">
<ref role="37wK5l" to="pgas:32CDcOz44ei" resolve="getIndexOfSortByName" />
<node concept="Xl_RD" id="4RJJaubT8gd" role="37wK5m">
<property role="Xl_RC" value="Context" />
</node>
</node>
</node>
</node>
</node>
<node concept="3cpWs8" id="4RJJaubTbFU" role="3cqZAp">
<node concept="3cpWsn" id="4RJJaubTbFV" role="3cpWs9">
<property role="TrG5h" value="newDeclaration" />
<node concept="3Tqbb2" id="4RJJaubTbFM" role="1tU5fm">
<ref role="ehGHo" to="b83y:2_58u12eLDI" resolve="JudgmentDeclaration" />
</node>
<node concept="2OqwBi" id="4RJJaubTbFW" role="33vP2m">
<node concept="37vLTw" id="4RJJaubTbFX" role="2Oq$k0">
<node concept="3clFbF" id="2iwoW_qE_tp" role="3cqZAp">
<node concept="2OqwBi" id="2iwoW_qE_z6" role="3clFbG">
<node concept="37vLTw" id="2iwoW_qE_tn" role="2Oq$k0">
<ref role="3cqZAo" node="32CDcOyFphS" resolve="projectContext" />
</node>
<node concept="liA8E" id="2iwoW_qE_De" role="2OqNvi">
<ref role="37wK5l" to="5tos:2iwoW_qDu_o" resolve="removeInfiniteNonUserSort" />
<node concept="37vLTw" id="2iwoW_qE_Ew" role="37wK5m">
<ref role="3cqZAo" node="4RJJauckL5H" resolve="decl" />
</node>
<node concept="2qgKlT" id="4RJJaubTbFY" role="2OqNvi">
<ref role="37wK5l" to="pgas:4XA4NEmJ4Wv" resolve="removeSort" />
<node concept="37vLTw" id="4RJJaubTbFZ" role="37wK5m">
<ref role="3cqZAo" node="4RJJaubT8g9" resolve="contextIndex" />
</node>
</node>
</node>
</node>
</node>
<node concept="3clFbF" id="4RJJaubSZlE" role="3cqZAp">
<node concept="2OqwBi" id="4RJJaubT0_g" role="3clFbG">
<node concept="37vLTw" id="6XUlM2o$L3B" role="2Oq$k0">
<ref role="3cqZAo" node="4RJJaubf6Wq" resolve="querier" />
</node>
<node concept="liA8E" id="4RJJaubT0MZ" role="2OqNvi">
<ref role="37wK5l" to="5tos:4RJJaubau1Z" resolve="replaceInstancesOfDeclaration" />
<node concept="37vLTw" id="4RJJaubT0Oh" role="37wK5m">
<ref role="3cqZAo" node="4RJJauckL5H" resolve="decl" />
</node>
<node concept="37vLTw" id="4RJJaubTeJ1" role="37wK5m">
<ref role="3cqZAo" node="4RJJaubTbFV" resolve="newDeclaration" />
</node>
</node>
</node>
</node>
......@@ -1540,7 +1515,7 @@
</node>
</node>
<node concept="37vLTw" id="4RJJauckL5J" role="1DdaDG">
<ref role="3cqZAo" node="32CDcOyFp_A" resolve="declsWithContextAndTerm" />
<ref role="3cqZAo" node="32CDcOyFp_A" resolve="declsWithUserAndNonUserInput" />
</node>
</node>
<node concept="3clFbH" id="32CDcOyO7vy" role="3cqZAp" />
......
......@@ -968,6 +968,100 @@
<ref role="2I9WkF" to="b83y:2U2uJPpd5x5" resolve="Sort" />
</node>
</node>
<node concept="13i0hz" id="2iwoW_qn2k0" role="13h7CS">
<property role="13i0iv" value="false" />
<property role="13i0it" value="false" />
<property role="TrG5h" value="getUserInputSorts" />
<node concept="3Tm1VV" id="2iwoW_qn2k1" role="1B3o_S" />
<node concept="3clFbS" id="2iwoW_qn2k2" role="3clF47">
<node concept="3clFbF" id="2iwoW_qn2k3" role="3cqZAp">
<node concept="2OqwBi" id="2iwoW_qn2k4" role="3clFbG">
<node concept="2OqwBi" id="2iwoW_qn2k5" role="2Oq$k0">
<node concept="BsUDl" id="2iwoW_qn2k6" role="2Oq$k0">
<ref role="37wK5l" node="4XA4NEmGQRd" resolve="getSorts" />
</node>
<node concept="3zZkjj" id="2iwoW_qn2k7" role="2OqNvi">
<node concept="1bVj0M" id="2iwoW_qn2k8" role="23t8la">
<node concept="3clFbS" id="2iwoW_qn2k9" role="1bW5cS">
<node concept="3clFbF" id="2iwoW_qn2ka" role="3cqZAp">
<node concept="2OqwBi" id="2iwoW_qn2kb" role="3clFbG">
<node concept="37vLTw" id="2iwoW_qn2kc" role="2Oq$k0">
<ref role="3cqZAo" node="2iwoW_qn2ke" resolve="it" />
</node>
<node concept="2qgKlT" id="2iwoW_qn42Y" role="2OqNvi">
<ref role="37wK5l" node="2iwoW_q825k" resolve="isUserInput" />
</node>
</node>
</node>
</node>
<node concept="Rh6nW" id="2iwoW_qn2ke" role="1bW2Oz">
<property role="TrG5h" value="it" />
<node concept="2jxLKc" id="2iwoW_qn2kf" role="1tU5fm" />
</node>
</node>
</node>
</node>
<node concept="ANE8D" id="2iwoW_qn2kg" role="2OqNvi" />
</node>
</node>
</node>
<node concept="2I9FWS" id="2iwoW_qn2kh" role="3clF45">
<ref role="2I9WkF" to="b83y:2U2uJPpd5x5" resolve="Sort" />
</node>
</node>
<node concept="13i0hz" id="2iwoW_qn4iq" role="13h7CS">
<property role="13i0iv" value="false" />
<property role="13i0it" value="false" />
<property role="TrG5h" value="getNonUserInputSorts" />
<node concept="3Tm1VV" id="2iwoW_qn4ir" role="1B3o_S" />
<node concept="3clFbS" id="2iwoW_qn4is" role="3clF47">
<node concept="3clFbF" id="2iwoW_qn4it" role="3cqZAp">
<node concept="2OqwBi" id="2iwoW_qn4iu" role="3clFbG">
<node concept="2OqwBi" id="2iwoW_qn4iv" role="2Oq$k0">
<node concept="BsUDl" id="2iwoW_qn4iw" role="2Oq$k0">
<ref role="37wK5l" node="4XA4NEmGQRd" resolve="getSorts" />
</node>
<node concept="3zZkjj" id="2iwoW_qn4ix" role="2OqNvi">
<node concept="1bVj0M" id="2iwoW_qn4iy" role="23t8la">
<node concept="3clFbS" id="2iwoW_qn4iz" role="1bW5cS">
<node concept="3clFbF" id="2iwoW_qn4i$" role="3cqZAp">
<node concept="1Wc70l" id="2iwoW_qn5l3" role="3clFbG">
<node concept="2OqwBi" id="2iwoW_qn5Cq" role="3uHU7B">
<node concept="37vLTw" id="2iwoW_qn5sy" role="2Oq$k0">
<ref role="3cqZAo" node="2iwoW_qn4iC" resolve="it" />
</node>
<node concept="2qgKlT" id="2iwoW_qn5W5" role="2OqNvi">
<ref role="37wK5l" node="2U2uJPpePaZ" resolve="isInfiniteInput" />
</node>
</node>
<node concept="3fqX7Q" id="2iwoW_qn5aj" role="3uHU7w">
<node concept="2OqwBi" id="2iwoW_qn5al" role="3fr31v">
<node concept="37vLTw" id="2iwoW_qn5am" role="2Oq$k0">
<ref role="3cqZAo" node="2iwoW_qn4iC" resolve="it" />
</node>
<node concept="2qgKlT" id="2iwoW_qn5an" role="2OqNvi">
<ref role="37wK5l" node="2iwoW_q825k" resolve="isUserInput" />
</node>
</node>
</node>
</node>
</node>
</node>
<node concept="Rh6nW" id="2iwoW_qn4iC" role="1bW2Oz">
<property role="TrG5h" value="it" />
<node concept="2jxLKc" id="2iwoW_qn4iD" role="1tU5fm" />
</node>
</node>
</node>
</node>
<node concept="ANE8D" id="2iwoW_qn4iE" role="2OqNvi" />
</node>
</node>
</node>
<node concept="2I9FWS" id="2iwoW_qn4iF" role="3clF45">
<ref role="2I9WkF" to="b83y:2U2uJPpd5x5" resolve="Sort" />
</node>
</node>
<node concept="13i0hz" id="2U2uJPpurJc" role="13h7CS">
<property role="13i0iv" value="false" />
<property role="13i0it" value="false" />
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment