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

add projection instances to rules and take do not construct terms in premises

parent adee1c96
......@@ -2504,6 +2504,7 @@
</node>
</node>
<node concept="3clFbH" id="7oauUztmQbs" role="3cqZAp" />
<node concept="3clFbH" id="7oauUzuq8hk" role="3cqZAp" />
<node concept="3SKdUt" id="7oauUztyzED" role="3cqZAp">
<node concept="3SKdUq" id="7oauUztyzEF" role="3SKWNk">
<property role="3SKdUp" value="create projection declarations for each infinite input that is non-user" />
......@@ -2725,8 +2726,136 @@
</node>
</node>
</node>
<node concept="3clFbH" id="7oauUztnuYW" role="3cqZAp" />
<node concept="3clFbH" id="7oauUztnAY$" role="3cqZAp" />
<node concept="3clFbH" id="7oauUzuD_Md" role="3cqZAp" />
<node concept="3SKdUt" id="7oauUzto3i1" role="3cqZAp">
<node concept="3SKdUq" id="7oauUzto3i3" role="3SKWNk">
<property role="3SKdUp" value="add projection instances to rules" />
</node>
</node>
<node concept="1DcWWT" id="7oauUzuqUhN" role="3cqZAp">
<node concept="3clFbS" id="7oauUzuqUhP" role="2LFqv$">
<node concept="3cpWs8" id="7oauUzur22i" role="3cqZAp">
<node concept="3cpWsn" id="7oauUzur22j" role="3cpWs9">
<property role="TrG5h" value="rulesOfDeclaration" />
<node concept="2I9FWS" id="7oauUzur22g" role="1tU5fm">
<ref role="2I9WkF" to="b83y:2_58u12eCWN" resolve="Rule" />
</node>
<node concept="2OqwBi" id="7oauUzur22k" role="33vP2m">
<node concept="37vLTw" id="7oauUzur22l" role="2Oq$k0">
<ref role="3cqZAo" node="7oauUzrT2MQ" resolve="querier" />
</node>
<node concept="liA8E" id="7oauUzur22m" role="2OqNvi">
<ref role="37wK5l" to="5tos:6XUlM2nL3i2" resolve="getRulesForDeclaration" />
<node concept="37vLTw" id="7oauUzur22n" role="37wK5m">
<ref role="3cqZAo" node="7oauUzuqUhQ" resolve="declaration" />
</node>
</node>
</node>
</node>
</node>
<node concept="3cpWs8" id="7oauUzurV93" role="3cqZAp">
<node concept="3cpWsn" id="7oauUzurV94" role="3cpWs9">
<property role="TrG5h" value="projectedSorts" />
<node concept="2I9FWS" id="7oauUzurV92" role="1tU5fm">
<ref role="2I9WkF" to="b83y:2U2uJPpd5x5" resolve="Sort" />
</node>
<node concept="2OqwBi" id="7oauUzurV95" role="33vP2m">
<node concept="37vLTw" id="7oauUzurV96" role="2Oq$k0">
<ref role="3cqZAo" node="7oauUzuqUhQ" resolve="declaration" />
</node>
<node concept="2qgKlT" id="7oauUzurV97" role="2OqNvi">
<ref role="37wK5l" to="pgas:2iwoW_qn4iq" resolve="getNonUserInputSorts" />
</node>
</node>
</node>
</node>
<node concept="1DcWWT" id="7oauUzur2bw" role="3cqZAp">
<node concept="3clFbS" id="7oauUzur2by" role="2LFqv$">
<node concept="1DcWWT" id="7oauUzurYqX" role="3cqZAp">
<node concept="3clFbS" id="7oauUzurYqZ" role="2LFqv$">
<node concept="3cpWs8" id="7oauUzus1Au" role="3cqZAp">
<node concept="3cpWsn" id="7oauUzus1Av" role="3cpWs9">
<property role="TrG5h" value="premise" />
<node concept="3Tqbb2" id="7oauUzus1At" role="1tU5fm">
<ref role="ehGHo" to="b83y:677Mj2_ELav" resolve="JudgmentInstanceWithDeclaration" />
</node>
<node concept="2OqwBi" id="7oauUzus1Aw" role="33vP2m">
<node concept="37vLTw" id="7oauUzus1Ax" role="2Oq$k0">
<ref role="3cqZAo" node="7oauUzsM84s" resolve="projectNonUserInput" />
</node>
<node concept="liA8E" id="7oauUzus1Ay" role="2OqNvi">
<ref role="37wK5l" to="5tos:7oauUzurMwI" resolve="createPremiseForProjectedDeclaration" />
<node concept="2OqwBi" id="7oauUzusbdD" role="37wK5m">
<node concept="37vLTw" id="7oauUzusa9M" role="2Oq$k0">
<ref role="3cqZAo" node="7oauUzur2bz" resolve="rule" />
</node>
<node concept="3TrEf2" id="7oauUzuscSe" role="2OqNvi">
<ref role="3Tt5mk" to="b83y:2_58u12eCXl" resolve="conclusion" />
</node>
</node>
<node concept="37vLTw" id="7oauUzus1A$" role="37wK5m">
<ref role="3cqZAo" node="7oauUzurYr0" resolve="sort" />
</node>
</node>
</node>
</node>
</node>
<node concept="3clFbF" id="7oauUzus1NC" role="3cqZAp">
<node concept="2OqwBi" id="7oauUzus44f" role="3clFbG">
<node concept="2OqwBi" id="7oauUzus1Xj" role="2Oq$k0">
<node concept="37vLTw" id="7oauUzus1NA" role="2Oq$k0">
<ref role="3cqZAo" node="7oauUzur2bz" resolve="rule" />
</node>
<node concept="3Tsc0h" id="7oauUzus2CZ" role="2OqNvi">
<ref role="3TtcxE" to="b83y:2_58u12eCWO" resolve="premises" />
</node>
</node>
<node concept="2Ke4WJ" id="7oauUzus6KT" role="2OqNvi">
<node concept="37vLTw" id="7oauUzus7EQ" role="25WWJ7">
<ref role="3cqZAo" node="7oauUzus1Av" resolve="premise" />
</node>
</node>
</node>
</node>
</node>
<node concept="3cpWsn" id="7oauUzurYr0" role="1Duv9x">
<property role="TrG5h" value="sort" />
<node concept="3Tqbb2" id="7oauUzurYzJ" role="1tU5fm">
<ref role="ehGHo" to="b83y:2U2uJPpd5x5" resolve="Sort" />
</node>
</node>
<node concept="37vLTw" id="7oauUzurYOS" role="1DdaDG">
<ref role="3cqZAo" node="7oauUzurV94" resolve="projectedSorts" />
</node>
</node>
</node>
<node concept="3cpWsn" id="7oauUzur2bz" role="1Duv9x">
<property role="TrG5h" value="rule" />
<node concept="3Tqbb2" id="7oauUzur2l8" role="1tU5fm">
<ref role="ehGHo" to="b83y:2_58u12eCWN" resolve="Rule" />
</node>
</node>
<node concept="37vLTw" id="7oauUzur2Hb" role="1DdaDG">
<ref role="3cqZAo" node="7oauUzur22j" resolve="rulesOfDeclaration" />
</node>
</node>
</node>
<node concept="3cpWsn" id="7oauUzuqUhQ" role="1Duv9x">
<property role="TrG5h" value="declaration" />
<node concept="3Tqbb2" id="7oauUzuqZcW" role="1tU5fm">
<ref role="ehGHo" to="b83y:2_58u12eLDI" resolve="JudgmentDeclaration" />
</node>
</node>
<node concept="2OqwBi" id="7oauUzuqZPE" role="1DdaDG">
<node concept="37vLTw" id="7oauUzuqZGZ" role="2Oq$k0">
<ref role="3cqZAo" node="7oauUzsM84s" resolve="projectNonUserInput" />
</node>
<node concept="2OwXpG" id="7oauUzur0Vv" role="2OqNvi">
<ref role="2Oxat5" to="5tos:7oauUztjDZd" resolve="projectedDeclarations" />
</node>
</node>
</node>
<node concept="3clFbH" id="7oauUzuD2ji" role="3cqZAp" />
<node concept="3SKdUt" id="7oauUztnIhp" role="3cqZAp">
<node concept="3SKdUq" id="7oauUztnIhr" role="3SKWNk">
<property role="3SKdUp" value="rewrite declarations that were the basis for the projections" />
......@@ -2863,17 +2992,11 @@
</node>
</node>
<node concept="3clFbH" id="7oauUztnPqv" role="3cqZAp" />
<node concept="3SKdUt" id="7oauUzto3i1" role="3cqZAp">
<node concept="3SKdUq" id="7oauUzto3i3" role="3SKWNk">
<property role="3SKdUp" value="TODO add projection instances to rules" />
</node>
</node>
<node concept="3SKdUt" id="7oauUzug3J0" role="3cqZAp">
<node concept="3SKdUq" id="7oauUzug3J2" role="3SKWNk">
<property role="3SKdUp" value="TODO generate no context lookup judgment" />
<node concept="3SKdUt" id="7oauUzv8_A$" role="3cqZAp">
<node concept="3SKdUq" id="7oauUzvlQLp" role="3SKWNk">
<property role="3SKdUp" value="TODO lookup no context" />
</node>
</node>
<node concept="3clFbH" id="7oauUztm8sS" role="3cqZAp" />
</node>
<node concept="3cpWsn" id="7oauUzrSZtl" role="1Duv9x">
<property role="TrG5h" value="module" />
......
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