Introduce Forall type. Refactor the typesystem to support forall/gen/inst, get rid of varname for every type var. Better editor.

This commit is contained in:
Fedor Isakov 2017-03-30 13:53:34 +02:00
parent 2f32a72527
commit cb2d735528
4 changed files with 1460 additions and 517 deletions

View File

@ -213,21 +213,11 @@
<ref role="13i0hy" to="tpcu:hEwIMiw" resolve="getPresentation" />
<node concept="3Tm1VV" id="3g9UT2j9IvG" role="1B3o_S" />
<node concept="3clFbS" id="3g9UT2j9IvH" role="3clF47">
<node concept="3clFbF" id="3g9UT2j9IzO" role="3cqZAp">
<node concept="3cpWs3" id="2OtUBGmkOUy" role="3clFbG">
<node concept="Xl_RD" id="2OtUBGmkOU_" role="3uHU7w">
<property role="Xl_RC" value="'" />
</node>
<node concept="3cpWs3" id="2OtUBGmkOiq" role="3uHU7B">
<node concept="Xl_RD" id="2OtUBGmkOit" role="3uHU7B">
<property role="Xl_RC" value="'" />
</node>
<node concept="2OqwBi" id="3g9UT2j9IHa" role="3uHU7w">
<node concept="13iPFW" id="3g9UT2j9IzN" role="2Oq$k0" />
<node concept="3TrcHB" id="3g9UT2j9IRP" role="2OqNvi">
<ref role="3TsBF5" to="8tt8:3g9UT2j9Itl" resolve="name" />
</node>
</node>
<node concept="3clFbF" id="12dHl3ZCh6s" role="3cqZAp">
<node concept="2OqwBi" id="3g9UT2j9IHa" role="3clFbG">
<node concept="13iPFW" id="3g9UT2j9IzN" role="2Oq$k0" />
<node concept="3TrcHB" id="3g9UT2j9IRP" role="2OqNvi">
<ref role="3TsBF5" to="8tt8:3g9UT2j9Itl" resolve="name" />
</node>
</node>
</node>
@ -235,5 +225,41 @@
<node concept="17QB3L" id="3g9UT2j9IvI" role="3clF45" />
</node>
</node>
<node concept="13h7C7" id="12dHl3ZCFbd">
<property role="3GE5qa" value="type" />
<ref role="13h7C2" to="8tt8:12dHl3ZCxTW" resolve="ForallType" />
<node concept="13hLZK" id="12dHl3ZCFbe" role="13h7CW">
<node concept="3clFbS" id="12dHl3ZCFbf" role="2VODD2" />
</node>
<node concept="13i0hz" id="12dHl3ZCFbo" role="13h7CS">
<property role="13i0is" value="false" />
<property role="TrG5h" value="getPresentation" />
<property role="13i0it" value="false" />
<property role="13i0iv" value="false" />
<ref role="13i0hy" to="tpcu:hEwIMiw" resolve="getPresentation" />
<node concept="3Tm1VV" id="12dHl3ZCFcx" role="1B3o_S" />
<node concept="3clFbS" id="12dHl3ZCFix" role="3clF47">
<node concept="3clFbF" id="12dHl3ZCFqk" role="3cqZAp">
<node concept="3cpWs3" id="12dHl3ZCFWS" role="3clFbG">
<node concept="2EnYce" id="12dHl3ZCJ3U" role="3uHU7w">
<node concept="2OqwBi" id="12dHl3ZCG91" role="2Oq$k0">
<node concept="13iPFW" id="12dHl3ZCFXg" role="2Oq$k0" />
<node concept="3TrEf2" id="12dHl3ZCGjV" role="2OqNvi">
<ref role="3Tt5mk" to="8tt8:12dHl3ZCFaI" resolve="type" />
</node>
</node>
<node concept="2qgKlT" id="12dHl3ZCJqZ" role="2OqNvi">
<ref role="37wK5l" to="tpcu:hEwIMiw" resolve="getPresentation" />
</node>
</node>
<node concept="Xl_RD" id="12dHl3ZCFqj" role="3uHU7B">
<property role="Xl_RC" value="forall." />
</node>
</node>
</node>
</node>
<node concept="17QB3L" id="12dHl3ZCFiy" role="3clF45" />
</node>
</node>
</model>

View File

@ -303,7 +303,7 @@
</node>
<node concept="24kQdi" id="7_8aRkgE08o">
<property role="3GE5qa" value="expr.fun" />
<ref role="1XX52x" to="8tt8:7_8aRkgDGQi" resolve="LamVarBinding" />
<ref role="1XX52x" to="8tt8:7_8aRkgDGQi" resolve="LamVarBind" />
<node concept="3EZMnI" id="7_8aRkgE08q" role="2wV5jI">
<node concept="3F0ifn" id="492bFERnr4S" role="3EZMnx">
<property role="3F0ifm" value="\" />
@ -411,7 +411,7 @@
<node concept="3cpWsn" id="3TFdEPZevrj" role="3cpWs9">
<property role="TrG5h" value="var" />
<node concept="3Tqbb2" id="3TFdEPZevrk" role="1tU5fm">
<ref role="ehGHo" to="8tt8:7_8aRkgDGQi" resolve="LamVarBinding" />
<ref role="ehGHo" to="8tt8:7_8aRkgDGQi" resolve="LamVarBind" />
</node>
<node concept="2OqwBi" id="3TFdEPZevrl" role="33vP2m">
<node concept="2OqwBi" id="3TFdEPZevrm" role="2Oq$k0">
@ -423,7 +423,7 @@
</node>
</node>
<node concept="2DeJnY" id="3TFdEPZevrp" role="2OqNvi">
<ref role="1A9B2P" to="8tt8:7_8aRkgDGQi" resolve="LamVarBinding" />
<ref role="1A9B2P" to="8tt8:7_8aRkgDGQi" resolve="LamVarBind" />
</node>
</node>
</node>
@ -590,7 +590,7 @@
</node>
<node concept="24kQdi" id="7_8aRkgFz03">
<property role="3GE5qa" value="" />
<ref role="1XX52x" to="8tt8:7_8aRkgDGQp" resolve="VarBinding" />
<ref role="1XX52x" to="8tt8:7_8aRkgDGQp" resolve="LetVarBind" />
<node concept="3EZMnI" id="7_8aRkgFz05" role="2wV5jI">
<node concept="3F1sOY" id="7_8aRkgFz0f" role="3EZMnx">
<ref role="1NtTu8" to="8tt8:7_8aRkgDGQq" resolve="var" />
@ -754,15 +754,9 @@
<property role="3GE5qa" value="type" />
<ref role="1XX52x" to="8tt8:3g9UT2j9I06" resolve="VarType" />
<node concept="3EZMnI" id="3g9UT2j9ItO" role="2wV5jI">
<node concept="3F0ifn" id="2OtUBGmkNrh" role="3EZMnx">
<property role="3F0ifm" value="'" />
</node>
<node concept="3F0A7n" id="3g9UT2j9ItV" role="3EZMnx">
<ref role="1NtTu8" to="8tt8:3g9UT2j9Itl" resolve="name" />
</node>
<node concept="3F0ifn" id="2OtUBGmkNrp" role="3EZMnx">
<property role="3F0ifm" value="'" />
</node>
<node concept="l2Vlx" id="3g9UT2j9ItR" role="2iSdaV" />
</node>
</node>
@ -782,5 +776,18 @@
<node concept="l2Vlx" id="7_zMfd$oooz" role="2iSdaV" />
</node>
</node>
<node concept="24kQdi" id="12dHl3ZCFav">
<property role="3GE5qa" value="type" />
<ref role="1XX52x" to="8tt8:12dHl3ZCxTW" resolve="ForallType" />
<node concept="3EZMnI" id="12dHl3ZCFax" role="2wV5jI">
<node concept="3F0ifn" id="12dHl3ZCFaC" role="3EZMnx">
<property role="3F0ifm" value="forall." />
</node>
<node concept="3F1sOY" id="12dHl3ZCFaK" role="3EZMnx">
<ref role="1NtTu8" to="8tt8:12dHl3ZCFaI" resolve="type" />
</node>
<node concept="l2Vlx" id="12dHl3ZCFa$" role="2iSdaV" />
</node>
</node>
</model>

View File

@ -315,5 +315,18 @@
<property role="EcuMT" value="4497748771651493439" />
<property role="TrG5h" value="Typeable" />
</node>
<node concept="1TIwiD" id="12dHl3ZCxTW">
<property role="EcuMT" value="1192808835813875324" />
<property role="3GE5qa" value="type" />
<property role="TrG5h" value="ForallType" />
<ref role="1TJDcQ" node="3_qfG1EP6Nw" resolve="Type" />
<node concept="1TJgyj" id="12dHl3ZCFaI" role="1TKVEi">
<property role="IQ2ns" value="1192808835813913262" />
<property role="20lmBu" value="aggregation" />
<property role="20kJfa" value="type" />
<property role="20lbJX" value="1" />
<ref role="20lvS9" node="3_qfG1EP6Nw" resolve="Type" />
</node>
</node>
</model>

File diff suppressed because it is too large Load Diff